Theorem dfbi2 479

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  dfbi  480  pm4.71  566  impimprbi  841  pm5.17  1027  xor  1030  dfbi3  1063  ifpdfbiOLD  1085  albiim  1916  nfbid  1929  sbbi  2348  ralbiim  3133  reu8  3705  dfss2  3931  soeq2  5592  fun11  6611  dffo3  7098  dffo3f  7102  isnsg2  19222  isarchi  33443  axextprim  36092  biimpexp  36108  axextndbi  36193  bj-nnfbit  37272  bj-nnfbid  37273  ifpidg  44109  ifp1bi  44120  ifpbibib  44128  rp-fakeanorass  44131  frege54cor0a  44481  aibandbiaiffaiffb  47520  aibandbiaiaiffb  47521  afv2orxorb  47854