Theorem dfbi2 480

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  dfbi  481  pm4.71  567  impimprbi  842  pm5.17  1029  xor  1032  dfbi3  1065  ifpdfbiOLD  1087  albiim  1922  nfbid  1935  sbbi  2340  ralbiim  3124  reu8  3691  dfss2  3917  soeq2  5585  fun11  6608  dffo3  7096  dffo3f  7100  isnsg2  19282  isarchi  33625  axextprim  36283  biimpexp  36299  axextndbi  36384  bj-nnfbit  37494  bj-nnfbid  37495  ifpidg  44334  ifp1bi  44345  ifpbibib  44353  rp-fakeanorass  44356  frege54cor0a  44706  aibandbiaiffaiffb  47785  aibandbiaiaiffb  47786  afv2orxorb  48119