Theorem adantll 694

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	|- ((ph /\ ps) -> ch)

Assertion

Ref	Expression
adantll	|- (((th /\ ph) /\ ps) -> ch)

Proof of Theorem adantll

Step	Hyp	Ref	Expression
1		simpr 447	. 2 |- ((th /\ ph) -> ph)
2		adant2.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	sylan 457	1 |- (((th /\ ph) /\ ps) -> ch)

Syntax hints:   -> wi 4   /\ wa 358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-an 360

This theorem is referenced by:  ad2antlr  707  ad2ant2l  726  ad2ant2lr  728  3ad2antl3  1119  3adant1l  1174  ax11eq  2193  ax11el  2194  nfeud2  2216  ralcom2  2775  reu6  3025  sbc2iegf  3112  sbcralt  3118  phialllem1  4616  imainss  5042  fun11iun  5305  eqfnfv  5392  foco2  5426  fconst2g  5452  isotr  5495  lemuc1  6253  nchoicelem17  6305