Theorem dfbi2 473

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  dfbi  474  pm4.71  556  impimprbi  827  pm5.17  1009  xor  1012  dfbi3  1047  ifpdfbi  1068  albiim  1884  nfbid  1897  sbbi  2297  ralbiim  3102  reu8  3726  dfss2  3964  sseq2  4005  soeq2  5615  fun11  6632  dffo3  7115  dffo3f  7119  isnsg2  19145  isarchi  33024  axextprim  35471  biimpexp  35487  axextndbi  35576  bj-nnfbit  36405  bj-nnfbid  36406  ifpidg  43095  ifp1bi  43106  ifpbibib  43114  rp-fakeanorass  43117  frege54cor0a  43467  aibandbiaiffaiffb  46446  aibandbiaiaiffb  46447  afv2orxorb  46778