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

Theorem dfbi2 462
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 204 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 df-an 385 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
31, 2bitr4i 269 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384
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 198  df-an 385
This theorem is referenced by:  dfbi  463  pm4.71  549  pm5.17  1026  xor  1029  dfbi3  1063  albiim  1978  nfbid  1994  nfbidOLD  2416  sbbi  2560  ralbiim  3257  reu8  3600  sseq2  3824  soeq2  5252  fun11  6174  dffo3  6596  isnsg2  17826  isarchi  30061  axextprim  31900  biimpexp  31919  axextndbi  32030  ifpdfbi  38318  ifpidg  38336  ifp1bi  38347  ifpbibib  38355  rp-fakeanorass  38358  frege54cor0a  38657  dffo3f  39853  aibandbiaiffaiffb  41543  aibandbiaiaiffb  41544  afv2orxorb  41817
  Copyright terms: Public domain W3C validator