New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  dfbi2 GIF 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-mp 5  ax-1 6  ax-2 7  ax-3 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