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  1013  xor  1016  dfbi3  1049  ifpdfbi  1070  albiim  1887  nfbid  1900  sbbi  2307  ralbiim  3111  reu8  3742  dfss2  3981  sseq2  4022  soeq2  5619  fun11  6642  dffo3  7122  dffo3f  7126  isnsg2  19187  isarchi  33172  axextprim  35681  biimpexp  35697  axextndbi  35786  bj-nnfbit  36735  bj-nnfbid  36736  ifpidg  43481  ifp1bi  43492  ifpbibib  43500  rp-fakeanorass  43503  frege54cor0a  43853  aibandbiaiffaiffb  46844  aibandbiaiaiffb  46845  afv2orxorb  47178