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  3100  reu8  3693  dfss2  3921  soeq2  5562  fun11  6574  dffo3  7056  dffo3f  7060  isnsg2  19097  isarchi  33276  axextprim  35917  biimpexp  35933  axextndbi  36018  bj-nnfbit  37001  bj-nnfbid  37002  ifpidg  43847  ifp1bi  43858  ifpbibib  43866  rp-fakeanorass  43869  frege54cor0a  44219  aibandbiaiffaiffb  47254  aibandbiaiaiffb  47255  afv2orxorb  47588