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  7681  prarloclemlo  7861  xrlttr  10197  fzen  10447  eluzgtdifelfzo  10615  ssfzo12bi  10643  climuni  12059  mulcn2  12078  serf0  12118  ntrivcvgap  12315  dfgcd2  12791  lcmgcdlem  12855  lcmdvds  12857  qnumdencl  12965  infpnlem1  13138  rng1zrlem  14258  cnplimcim  15768  dveflem  15827  gausslemma2dlem3  16182  uhgr2edg  16447  ushgredgedg  16467  ushgredgedgloop  16469  wlk1walkdom  16600  clwwlknun  16682  bj-charfundcALT  16835