NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  syl2anb Unicode 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-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:  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