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  709  dedlema  953  dedlemb  954  prlem1  957  equveli  1732  poxp  6129  nnmordi  6412  eroprf  6522  xpdom2  6725  elni2  7122  prarloclemlo  7302  xrlttr  9581  fzen  9823  eluzgtdifelfzo  9974  ssfzo12bi  10002  climuni  11062  mulcn2  11081  serf0  11121  ntrivcvgap  11317  dfgcd2  11702  lcmgcdlem  11758  lcmdvds  11760  qnumdencl  11865  cnplimcim  12805  dveflem  12855