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  2776  reu6  3026  sbc2iegf  3113  sbcralt  3119  phialllem1  4617  imainss  5043  fun11iun  5306  eqfnfv  5393  foco2  5427  fconst2g  5453  isotr  5496  lemuc1  6254  nchoicelem17  6306