New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  adantlr GIF version

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 ((φ ψ) → χ)
Assertion
Ref Expression
adantlr (((φ θ) ψ) → χ)

Proof of Theorem adantlr
StepHypRef Expression
1 simpl 443 . 2 ((φ θ) → φ)
2 adant2.1 . 2 ((φ ψ) → χ)
31, 2sylan 457 1 (((φ θ) ψ) → χ)
 Colors of variables: wff setvar class 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
 Copyright terms: Public domain W3C validator