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

Theorem dfbi2 473
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 212 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 df-an 395 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
31, 2bitr4i 277 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394
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 206  df-an 395
This theorem is referenced by:  dfbi  474  pm4.71  556  impimprbi  827  pm5.17  1009  xor  1012  dfbi3  1047  ifpdfbi  1068  albiim  1884  nfbid  1897  sbbi  2297  ralbiim  3102  reu8  3726  dfss2  3964  sseq2  4005  soeq2  5615  fun11  6632  dffo3  7115  dffo3f  7119  isnsg2  19145  isarchi  33024  axextprim  35471  biimpexp  35487  axextndbi  35576  bj-nnfbit  36405  bj-nnfbid  36406  ifpidg  43095  ifp1bi  43106  ifpbibib  43114  rp-fakeanorass  43117  frege54cor0a  43467  aibandbiaiffaiffb  46446  aibandbiaiaiffb  46447  afv2orxorb  46778
  Copyright terms: Public domain W3C validator