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

Theorem dfbi2 661
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 203 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 df-an 385 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
31, 2bitr4i 267 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  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 197  df-an 385
This theorem is referenced by:  dfbi  662  pm4.71  663  pm5.17  950  xor  953  dfbi3  1018  albiim  1856  nfbid  1872  nfbidOLD  2278  sbbi  2429  ralbiim  3098  reu8  3435  sseq2  3660  soeq2  5084  fun11  6001  dffo3  6414  isnsg2  17671  isarchi  29864  axextprim  31704  biimpexp  31723  axextndbi  31834  ifpdfbi  38135  ifpidg  38153  ifp1bi  38164  ifpbibib  38172  rp-fakeanorass  38175  frege54cor0a  38474  dffo3f  39678  aibandbiaiffaiffb  41382  aibandbiaiaiffb  41383
  Copyright terms: Public domain W3C validator