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

Theorem dfbi2 658
 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 202 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 df-an 385 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
31, 2bitr4i 266 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  dfbi  659  pm4.71  660  pm5.17  928  xor  931  albiim  1806  nfbid  1820  nfbidOLD  2230  sbbi  2389  ralbiim  3051  reu8  3369  sseq2  3590  soeq2  4979  fun11  5877  dffo3  6282  isnsg2  17447  isarchi  29067  axextprim  30832  biimpexp  30852  axextndbi  30954  ifpdfbi  36837  ifpidg  36855  ifp1bi  36866  ifpbibib  36874  rp-fakeanorass  36877  frege54cor0a  37177  dffo3f  38359  aibandbiaiffaiffb  39710  aibandbiaiaiffb  39711
 Copyright terms: Public domain W3C validator