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  3680  dfss2  3908  soeq2  5555  fun11  6567  dffo3  7049  dffo3f  7053  isnsg2  19125  isarchi  33261  axextprim  35902  biimpexp  35918  axextndbi  36003  bj-nnfbit  37074  bj-nnfbid  37075  ifpidg  43939  ifp1bi  43950  ifpbibib  43958  rp-fakeanorass  43961  frege54cor0a  44311  aibandbiaiffaiffb  47357  aibandbiaiaiffb  47358  afv2orxorb  47691