Theorem adantld 278

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 110	. 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 104

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

This theorem is referenced by:  jaoa  728  dedlema  978  dedlemb  979  prlem1  982  equveli  1807  ifnebibdc  3655  poxp  6406  ressuppss  6432  nnmordi  6727  eroprf  6840  xpdom2  7058  elni2  7594  prarloclemlo  7774  xrlttr  10091  fzen  10340  eluzgtdifelfzo  10505  ssfzo12bi  10533  climuni  11933  mulcn2  11952  serf0  11992  ntrivcvgap  12189  dfgcd2  12665  lcmgcdlem  12729  lcmdvds  12731  qnumdencl  12839  infpnlem1  13012  cnplimcim  15478  dveflem  15537  gausslemma2dlem3  15882  uhgr2edg  16147  ushgredgedg  16167  ushgredgedgloop  16169  wlk1walkdom  16300  clwwlknun  16382  bj-charfundcALT  16525