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  14342  cnplimcim  15859  dveflem  15918  gausslemma2dlem3  16348  uhgr2edg  16613  ushgredgedg  16633  ushgredgedgloop  16635  wlk1walkdom  16766  clwwlknun  16848  bj-charfundcALT  17001