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

Theorem syl2anb 465
 Description: A double syllogism inference. (Contributed by NM, 29-Jul-1999.)
Hypotheses
Ref Expression
syl2anb.1 (φψ)
syl2anb.2 (τχ)
syl2anb.3 ((ψ χ) → θ)
Assertion
Ref Expression
syl2anb ((φ τ) → θ)

Proof of Theorem syl2anb
StepHypRef Expression
1 syl2anb.2 . 2 (τχ)
2 syl2anb.1 . . 3 (φψ)
3 syl2anb.3 . . 3 ((ψ χ) → θ)
42, 3sylanb 458 . 2 ((φ χ) → θ)
51, 4sylan2b 461 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:  sylancb  646  2eu6  2289  reupick3  3540  difprsnss  3846  ncfinraise  4481  ncfinlower  4483  sfinltfin  4535  fnun  5189  f1oun  5304  eqfunfv  5397  swapf1o  5511  fnfullfunlem2  5857  fvfullfunlem3  5863  xpassen  6057  enprmaplem3  6078  ncaddccl  6144  peano4nc  6150  cenc  6181
 Copyright terms: Public domain W3C validator