MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfbi2 Structured version   Visualization version   GIF version

Theorem dfbi2 467
Description: A theorem similar to the standard definition of the biconditional. Definition of [Margaris] p. 49. (Contributed by NM, 24-Jan-1993.)
Assertion
Ref Expression
dfbi2 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))

Proof of Theorem dfbi2
StepHypRef Expression
1 dfbi1 205 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 df-an 388 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
31, 2bitr4i 270 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387
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 199  df-an 388
This theorem is referenced by:  dfbi  468  pm4.71  550  pm5.17  994  xor  997  dfbi3  1030  albiim  1852  nfbid  1865  sbbi  2241  sbbivOLD  2250  sbbiALT  2538  eu6OLDOLD  2593  ralbiim  3124  reu8  3636  sseq2  3883  soeq2  5347  fun11  6261  dffo3  6691  isnsg2  18093  isarchi  30483  axextprim  32453  biimpexp  32472  axextndbi  32576  ifpdfbi  39241  ifpidg  39259  ifp1bi  39270  ifpbibib  39278  rp-fakeanorass  39281  frege54cor0a  39578  dffo3f  40868  aibandbiaiffaiffb  42566  aibandbiaiaiffb  42567  afv2orxorb  42839
  Copyright terms: Public domain W3C validator