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  1808  ifnebibdc  3672  poxp  6441  ressuppss  6467  nnmordi  6762  eroprf  6875  xpdom2  7095  elni2  7645  prarloclemlo  7825  xrlttr  10147  fzen  10397  eluzgtdifelfzo  10564  ssfzo12bi  10592  climuni  12003  mulcn2  12022  serf0  12062  ntrivcvgap  12259  dfgcd2  12735  lcmgcdlem  12799  lcmdvds  12801  qnumdencl  12909  infpnlem1  13082  rng1zrlem  14198  cnplimcim  15658  dveflem  15717  gausslemma2dlem3  16062  uhgr2edg  16327  ushgredgedg  16347  ushgredgedgloop  16349  wlk1walkdom  16480  clwwlknun  16562  bj-charfundcALT  16705