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

Theorem syl5bir 209
Description: A mixed syllogism inference from a nested implication and a biconditional. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bir.1
syl5bir.2
Assertion
Ref Expression
syl5bir

Proof of Theorem syl5bir
StepHypRef Expression
1 syl5bir.1 . . 3
21biimpri 197 . 2
3 syl5bir.2 . 2
42, 3syl5 28 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:  3imtr3g  260  oplem1  930  nic-ax  1438  19.30  1604  19.33b  1608  ax10  1944  necon4bd  2578  ceqex  2969  ssdisj  3600  pssdifn0  3611  ltfintr  4459  evenodddisj  4516  sfinltfin  4535  fun11iun  5305  funopfv  5357  dff3  5420  funfvima  5459  trrd  5925  peano4nc  6150  ncspw1eu  6159  fce  6188
  Copyright terms: Public domain W3C validator