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  1921  nfbid  1934  sbbi  2340  ralbiim  3124  reu8  3690  dfss2  4093  soeq2  5581  fun11  6619  dffo3  7107  dffo3f  7111  isnsg2  19375  isarchi  33793  axextprim  36590  biimpexp  36606  axextndbi  36690  bj-nnfbit  37784  bj-nnfbid  37785  ifpidg  44629  ifp1bi  44640  ifpbibib  44648  rp-fakeanorass  44651  frege54cor0a  45000  aibandbiaiffaiffb  48100  aibandbiaiaiffb  48101  afv2orxorb  48434