Theorem dfbi2 661

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 385	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
3	1, 2	bitr4i 267	1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383

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 385

This theorem is referenced by:  dfbi  662  pm4.71  663  pm5.17  950  xor  953  dfbi3  1018  albiim  1856  nfbid  1872  nfbidOLD  2278  sbbi  2429  ralbiim  3098  reu8  3435  sseq2  3660  soeq2  5084  fun11  6001  dffo3  6414  isnsg2  17671  isarchi  29864  axextprim  31704  biimpexp  31723  axextndbi  31834  ifpdfbi  38135  ifpidg  38153  ifp1bi  38164  ifpbibib  38172  rp-fakeanorass  38175  frege54cor0a  38474  dffo3f  39678  aibandbiaiffaiffb  41382  aibandbiaiaiffb  41383