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  725  dedlema  975  dedlemb  976  prlem1  979  equveli  1805  ifnebibdc  3648  poxp  6384  nnmordi  6670  eroprf  6783  xpdom2  6998  elni2  7512  prarloclemlo  7692  xrlttr  10003  fzen  10251  eluzgtdifelfzo  10415  ssfzo12bi  10443  climuni  11820  mulcn2  11839  serf0  11879  ntrivcvgap  12075  dfgcd2  12551  lcmgcdlem  12615  lcmdvds  12617  qnumdencl  12725  infpnlem1  12898  cnplimcim  15357  dveflem  15416  gausslemma2dlem3  15758  uhgr2edg  16020  ushgredgedg  16040  ushgredgedgloop  16042  wlk1walkdom  16105  bj-charfundcALT  16255