Theorem adantld 263

Description: Deduction adding a conjunct to the left of an antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 20-Dec-2012.)

Hypothesis

Ref	Expression
adantld.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
adantld	|- ( ph -> ( ( th /\ ps ) -> ch ) )

Proof of Theorem adantld

Step	Hyp	Ref	Expression
1		simpr 103	. 2 |- ( ( th /\ ps ) -> ps )
2		adantld.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 28	1 |- ( ph -> ( ( th /\ ps ) -> ch ) )

Syntax hints:   -> wi 4   /\ wa 97

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100

This theorem is referenced by:  jaoa  640  dedlema  876  dedlemb  877  prlem1  880  equveli  1642  poxp  5853  nnmordi  6089  eroprf  6199  xpdom2  6305  elni2  6412  prarloclemlo  6592  xrlttr  8716  fzen  8907  eluzgtdifelfzo  9053  ssfzo12bi  9081  climuni  9814  mulcn2  9833  serif0  9871