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

Theorem sylanb 458
Description: A syllogism inference. (Contributed by NM, 18-May-1994.)
Hypotheses
Ref Expression
sylanb.1
sylanb.2
Assertion
Ref Expression
sylanb

Proof of Theorem sylanb
StepHypRef Expression
1 sylanb.1 . . 3
21biimpi 186 . 2
3 sylanb.2 . 2
42, 3sylan 457 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  anabsan  786  eqtr2  2371  pm13.181  2589  rmob  3134  sspsstr  3374  disjne  3596  xpcan2  5058  fssres  5238  funbrfvb  5360  fvco  5383  fvimacnvi  5402  ffvresb  5431  leaddc2  6215  lemuc2  6254
  Copyright terms: Public domain W3C validator