Theorem dfbi2 660

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

Step	Hyp	Ref	Expression
1		dfbi1 203	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		df-an 386	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
3	1, 2	bitr4i 267	1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ 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 197  df-an 386

This theorem is referenced by:  dfbi  661  pm4.71  662  pm5.17  932  xor  935  dfbi3  994  albiim  1816  nfbid  1832  nfbidOLD  2242  sbbi  2401  ralbiim  3069  reu8  3402  sseq2  3627  soeq2  5055  fun11  5963  dffo3  6374  isnsg2  17624  isarchi  29736  axextprim  31578  biimpexp  31597  axextndbi  31710  ifpdfbi  37818  ifpidg  37836  ifp1bi  37847  ifpbibib  37855  rp-fakeanorass  37858  frege54cor0a  38157  dffo3f  39364  aibandbiaiffaiffb  41061  aibandbiaiaiffb  41062