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  710  dedlema  954  dedlemb  955  prlem1  958  equveli  1736  poxp  6169  nnmordi  6452  eroprf  6562  xpdom2  6765  elni2  7213  prarloclemlo  7393  xrlttr  9680  fzen  9923  eluzgtdifelfzo  10074  ssfzo12bi  10102  climuni  11167  mulcn2  11186  serf0  11226  ntrivcvgap  11422  dfgcd2  11869  lcmgcdlem  11925  lcmdvds  11927  qnumdencl  12032  cnplimcim  12975  dveflem  13026  bj-charfundcALT  13322