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

Theorem dfbi2 478
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 216 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 df-an 400 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
31, 2bitr4i 281 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399
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 210  df-an 400
This theorem is referenced by:  dfbi  479  pm4.71  561  impimprbi  827  pm5.17  1009  xor  1012  dfbi3  1045  ifpdfbi  1066  norassOLD  1535  albiim  1890  nfbid  1903  sbbi  2315  sbbivOLD  2322  sbbiALT  2590  ralbiim  3144  reu8  3675  sseq2  3944  soeq2  5463  fun11  6402  dffo3  6849  isnsg2  18304  isarchi  30865  axextprim  33041  biimpexp  33060  axextndbi  33163  bj-nnfbit  34197  bj-nnfbid  34198  andiff  39377  ifpidg  40192  ifp1bi  40203  ifpbibib  40211  rp-fakeanorass  40214  frege54cor0a  40557  dffo3f  41799  aibandbiaiffaiffb  43480  aibandbiaiaiffb  43481  afv2orxorb  43777
  Copyright terms: Public domain W3C validator