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

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is referenced by:  jaoa  722  dedlema  972  dedlemb  973  prlem1  976  equveli  1782  ifnebibdc  3615  poxp  6320  nnmordi  6604  eroprf  6717  xpdom2  6928  elni2  7429  prarloclemlo  7609  xrlttr  9919  fzen  10167  eluzgtdifelfzo  10328  ssfzo12bi  10356  climuni  11637  mulcn2  11656  serf0  11696  ntrivcvgap  11892  dfgcd2  12368  lcmgcdlem  12432  lcmdvds  12434  qnumdencl  12542  infpnlem1  12715  cnplimcim  15172  dveflem  15231  gausslemma2dlem3  15573  bj-charfundcALT  15782