Theorem adantld 272

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 108	. 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 102

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

This theorem is referenced by:  jaoa  673  dedlema  911  dedlemb  912  prlem1  915  equveli  1684  poxp  5905  nnmordi  6177  eroprf  6287  xpdom2  6397  elni2  6636  prarloclemlo  6816  xrlttr  9016  fzen  9208  eluzgtdifelfzo  9353  ssfzo12bi  9381  climuni  10351  mulcn2  10370  serif0  10408  dfgcd2  10628  lcmgcdlem  10684  lcmdvds  10686  qnumdencl  10790