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  6472  ressuppss  6498  nnmordi  6794  eroprf  6907  xpdom2  7135  elni2  7687  prarloclemlo  7867  xrlttr  10213  fzen  10463  eluzgtdifelfzo  10631  ssfzo12bi  10659  climuni  12083  mulcn2  12102  serf0  12142  ntrivcvgap  12339  dfgcd2  12815  lcmgcdlem  12879  lcmdvds  12881  qnumdencl  12991  infpnlem1  13166  prmlem1  13250  prmlem2  13262  rng1zrlem  14364  cnplimcim  15910  dveflem  15969  gausslemma2dlem3  16404  uhgr2edg  16669  ushgredgedg  16689  ushgredgedgloop  16691  wlk1walkdom  16822  clwwlknun  16904  bj-charfundcALT  17057