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  6793  eroprf  6906  xpdom2  7133  elni2  7687  prarloclemlo  7867  xrlttr  10214  fzen  10464  eluzgtdifelfzo  10632  ssfzo12bi  10660  climuni  12084  mulcn2  12103  serf0  12143  ntrivcvgap  12340  dfgcd2  12816  lcmgcdlem  12880  lcmdvds  12882  qnumdencl  12992  infpnlem1  13167  prmlem1  13251  prmlem2  13263  rng1zrlem  14365  cnplimcim  15893  dveflem  15952  gausslemma2dlem3  16387  uhgr2edg  16652  ushgredgedg  16672  ushgredgedgloop  16674  wlk1walkdom  16805  clwwlknun  16887  bj-charfundcALT  17040