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

Theorem bi1 178
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)
Assertion
Ref Expression
bi1

Proof of Theorem bi1
StepHypRef Expression
1 df-bi 177 . . 3
2 simplim 143 . . 3
31, 2ax-mp 5 . 2
4 simplim 143 . 2
53, 4syl 15 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   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:  biimpi  186  bicom1  190  biimpd  198  ibd  234  pm5.74  235  bi3ant  280  pm5.501  330  bija  344  albi  1564  exbi  1581  cbv2h  1980  sbied  2036  eumo0  2228  2eu6  2289  ceqsalt  2881  vtoclgft  2905  spcgft  2931  pm13.183  2979  reu6  3025  reu3  3026  sbciegft  3076  fv3  5341
  Copyright terms: Public domain W3C validator