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

Theorem dfbi2 609
Description: A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
dfbi2

Proof of Theorem dfbi2
StepHypRef Expression
1 dfbi1 184 . 2
2 df-an 360 . 2
31, 2bitr4i 243 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   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:  dfbi  610  pm4.71  611  pm5.17  858  xor  861  albiim  1611  nfbid  1832  nfbiOLD  1835  sbbi  2071  cleqh  2450  ralbiim  2751  reu8  3032  sseq2  3293  funeq  5127  fun11  5159  dffo3  5422
  Copyright terms: Public domain W3C validator