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  2595  pm2.61da3ne  2596  uneqdifeq  3638  intab  3956  leltfintr  4458  phi11lem1  4595  phialllem1  4616  fun11iun  5305  eqfnfv  5392  fconst2g  5452  isocnv  5491  isotr  5495  fvfullfunlem3  5863  dflec2  6210  tlecg  6230  ncslesuc  6267  nchoicelem19  6307