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

Theorem syl5bbr 250
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bbr.1
syl5bbr.2
Assertion
Ref Expression
syl5bbr

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3
21bicomi 193 . 2
3 syl5bbr.2 . 2
42, 3syl5bb 248 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wb 176
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
This theorem is referenced by:  3bitr3g  278  biass  348  19.16  1860  19.19  1862  sbco2  2086  cbvab  2471  necon1bbid  2570  necon4abid  2580  elabgt  2982  sbceq1a  3056  sbcralt  3118  sbccsbg  3164  sbccsb2g  3165  opkelimagekg  4271  vfin1cltv  4547  phialllem1  4616  phiall  4618  xp11  5056  nfunv  5138  fnssresb  5195  fun11iun  5305  dffo4  5423  elunirn  5470  isomin  5496  resoprab2  5582  nchoicelem11  6299
  Copyright terms: Public domain W3C validator