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  6318  nnmordi  6602  eroprf  6715  xpdom2  6926  elni2  7427  prarloclemlo  7607  xrlttr  9917  fzen  10165  eluzgtdifelfzo  10326  ssfzo12bi  10354  climuni  11604  mulcn2  11623  serf0  11663  ntrivcvgap  11859  dfgcd2  12335  lcmgcdlem  12399  lcmdvds  12401  qnumdencl  12509  infpnlem1  12682  cnplimcim  15139  dveflem  15198  gausslemma2dlem3  15540  bj-charfundcALT  15745