Theorem dfbi2 474

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 213	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		df-an 396	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
3	1, 2	bitr4i 278	1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  dfbi  475  pm4.71  557  impimprbi  829  pm5.17  1014  xor  1017  dfbi3  1050  ifpdfbi  1071  albiim  1891  nfbid  1904  sbbi  2314  ralbiim  3099  reu8  3679  dfss2  3907  soeq2  5561  fun11  6572  dffo3  7054  dffo3f  7058  isnsg2  19131  isarchi  33243  axextprim  35883  biimpexp  35899  axextndbi  35984  bj-nnfbit  37055  bj-nnfbid  37056  ifpidg  43918  ifp1bi  43929  ifpbibib  43937  rp-fakeanorass  43940  frege54cor0a  44290  aibandbiaiffaiffb  47342  aibandbiaiaiffb  47343  afv2orxorb  47676