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  720  dedlema  969  dedlemb  970  prlem1  973  equveli  1759  poxp  6235  nnmordi  6519  eroprf  6630  xpdom2  6833  elni2  7315  prarloclemlo  7495  xrlttr  9797  fzen  10045  eluzgtdifelfzo  10199  ssfzo12bi  10227  climuni  11303  mulcn2  11322  serf0  11362  ntrivcvgap  11558  dfgcd2  12017  lcmgcdlem  12079  lcmdvds  12081  qnumdencl  12189  infpnlem1  12359  cnplimcim  14221  dveflem  14272  bj-charfundcALT  14646