Theorem adantld 276

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 109	. 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 103

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

This theorem is referenced by:  jaoa  715  dedlema  964  dedlemb  965  prlem1  968  equveli  1752  poxp  6211  nnmordi  6495  eroprf  6606  xpdom2  6809  elni2  7276  prarloclemlo  7456  xrlttr  9752  fzen  9999  eluzgtdifelfzo  10153  ssfzo12bi  10181  climuni  11256  mulcn2  11275  serf0  11315  ntrivcvgap  11511  dfgcd2  11969  lcmgcdlem  12031  lcmdvds  12033  qnumdencl  12141  infpnlem1  12311  cnplimcim  13430  dveflem  13481  bj-charfundcALT  13844