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

Theorem dfbi2 475
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 214 . 2 ((𝜑𝜓) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
2 df-an 397 . 2 (((𝜑𝜓) ∧ (𝜓𝜑)) ↔ ¬ ((𝜑𝜓) → ¬ (𝜓𝜑)))
31, 2bitr4i 279 1 ((𝜑𝜓) ↔ ((𝜑𝜓) ∧ (𝜓𝜑)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396
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 208  df-an 397
This theorem is referenced by:  dfbi  476  pm4.71  558  impimprbi  824  pm5.17  1005  xor  1008  dfbi3  1041  norassOLD  1525  albiim  1881  nfbid  1894  sbbi  2308  sbbivOLD  2318  sbbiALT  2604  ralbiim  3171  reu8  3721  sseq2  3990  soeq2  5488  fun11  6421  dffo3  6860  isnsg2  18246  isarchi  30738  axextprim  32824  biimpexp  32843  axextndbi  32946  bj-nnfbit  33978  bj-nnfbid  33979  ifpdfbi  39717  ifpidg  39735  ifp1bi  39746  ifpbibib  39754  rp-fakeanorass  39757  frege54cor0a  40087  dffo3f  41314  aibandbiaiffaiffb  43007  aibandbiaiaiffb  43008  afv2orxorb  43304
  Copyright terms: Public domain W3C validator