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  675  dedlema  915  dedlemb  916  prlem1  919  equveli  1689  poxp  5997  nnmordi  6275  eroprf  6385  xpdom2  6547  elni2  6873  prarloclemlo  7053  xrlttr  9265  fzen  9457  eluzgtdifelfzo  9608  ssfzo12bi  9636  climuni  10681  mulcn2  10701  serf0  10741  dfgcd2  11281  lcmgcdlem  11337  lcmdvds  11339  qnumdencl  11443