Theorem adantlr 695

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
adantlr	|- (((ph /\ th) /\ ps) -> ch)

Proof of Theorem adantlr

Step	Hyp	Ref	Expression
1		simpl 443	. 2 |- ((ph /\ th) -> ph)
2		adant2.1	. 2 |- ((ph /\ ps) -> ch)
3	1, 2	sylan 457	1 |- (((ph /\ th) /\ 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:  ad2antrr  706  ad2ant2r  727  ad2ant2rl  729  pm2.61ddan  767  pm2.61dda  768  3ad2antl1  1117  3ad2antl2  1118  3adant1r  1175  ax11eq  2193  ax11el  2194  ax11indalem  2197  ax11inda2ALT  2198  nfeud2  2216  pm2.61da2ne  2596  pm2.61da3ne  2597  uneqdifeq  3639  intab  3957  leltfintr  4459  phi11lem1  4596  phialllem1  4617  fun11iun  5306  eqfnfv  5393  fconst2g  5453  isocnv  5492  isotr  5496  fvfullfunlem3  5864  dflec2  6211  tlecg  6231  ncslesuc  6268  nchoicelem19  6308