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

Theorem sylan2b 461
 Description: A syllogism inference. (Contributed by NM, 21-Apr-1994.)
Hypotheses
Ref Expression
sylan2b.1 (φχ)
sylan2b.2 ((ψ χ) → θ)
Assertion
Ref Expression
sylan2b ((ψ φ) → θ)

Proof of Theorem sylan2b
StepHypRef Expression
1 sylan2b.1 . . 3 (φχ)
21biimpi 186 . 2 (φχ)
3 sylan2b.2 . 2 ((ψ χ) → θ)
42, 3sylan2 460 1 ((ψ φ) → θ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 176   ∧ wa 358 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-an 360 This theorem is referenced by:  syl2anb  465  bm1.1  2338  eqtr3  2372  morex  3020  psssstr  3375  reuss2  3535  reupick  3539  reximdva0  3561  rabsneu  3795  reiota2  4368  nnsucelr  4428  nndisjeq  4429  prepeano4  4451  lefinlteq  4463  ltlefin  4468  ncfinraise  4481  sfindbl  4530  nulnnn  4556  xpcan  5057  fnfco  5237  fun11iun  5305  tz6.12-1  5344  fnressn  5438  fndmeng  6046
 Copyright terms: Public domain W3C validator