Theorem adantld 276

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 109	. 2 |- ( ( th /\ ps ) -> ps )
2		adantld.1	. 2 |- ( ph -> ( ps -> ch ) )
3	1, 2	syl5 32	1 |- ( ph -> ( ( th /\ ps ) -> ch ) )

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  jaoa  710  dedlema  959  dedlemb  960  prlem1  963  equveli  1747  poxp  6200  nnmordi  6484  eroprf  6594  xpdom2  6797  elni2  7255  prarloclemlo  7435  xrlttr  9731  fzen  9978  eluzgtdifelfzo  10132  ssfzo12bi  10160  climuni  11234  mulcn2  11253  serf0  11293  ntrivcvgap  11489  dfgcd2  11947  lcmgcdlem  12009  lcmdvds  12011  qnumdencl  12119  infpnlem1  12289  cnplimcim  13276  dveflem  13327  bj-charfundcALT  13691