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 ) )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is used by:  jaoa  732  dedlema  982  dedlemb  983  prlem1  986  equveli  1812  ifnebibdc  3686  poxp  6468  ressuppss  6494  nnmordi  6789  eroprf  6902  xpdom2  7129  elni2  7682  prarloclemlo  7862  xrlttr  10208  fzen  10458  eluzgtdifelfzo  10626  ssfzo12bi  10654  climuni  12078  mulcn2  12097  serf0  12137  ntrivcvgap  12334  dfgcd2  12810  lcmgcdlem  12874  lcmdvds  12876  qnumdencl  12986  infpnlem1  13161  prmlem1  13245  prmlem2  13257  rng1zrlem  14349  cnplimcim  15867  dveflem  15926  gausslemma2dlem3  16361  uhgr2edg  16626  ushgredgedg  16646  ushgredgedgloop  16648  wlk1walkdom  16779  clwwlknun  16861  bj-charfundcALT  17014