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  721  dedlema  971  dedlemb  972  prlem1  975  equveli  1770  ifnebibdc  3601  poxp  6287  nnmordi  6571  eroprf  6684  xpdom2  6887  elni2  7376  prarloclemlo  7556  xrlttr  9864  fzen  10112  eluzgtdifelfzo  10267  ssfzo12bi  10295  climuni  11439  mulcn2  11458  serf0  11498  ntrivcvgap  11694  dfgcd2  12154  lcmgcdlem  12218  lcmdvds  12220  qnumdencl  12328  infpnlem1  12500  cnplimcim  14846  dveflem  14905  gausslemma2dlem3  15220  bj-charfundcALT  15371