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  6378  nnmordi  6662  eroprf  6775  xpdom2  6990  elni2  7501  prarloclemlo  7681  xrlttr  9991  fzen  10239  eluzgtdifelfzo  10403  ssfzo12bi  10431  climuni  11804  mulcn2  11823  serf0  11863  ntrivcvgap  12059  dfgcd2  12535  lcmgcdlem  12599  lcmdvds  12601  qnumdencl  12709  infpnlem1  12882  cnplimcim  15341  dveflem  15400  gausslemma2dlem3  15742  uhgr2edg  16004  ushgredgedg  16024  ushgredgedgloop  16026  wlk1walkdom  16070  bj-charfundcALT  16172