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  2341  ralbiim  3125  reu8  3691  dfss2  3917  soeq2  5581  fun11  6614  dffo3  7102  dffo3f  7106  isnsg2  19366  isarchi  33743  axextprim  36466  biimpexp  36482  axextndbi  36566  bj-nnfbit  37660  bj-nnfbid  37661  ifpidg  44491  ifp1bi  44502  ifpbibib  44510  rp-fakeanorass  44513  frege54cor0a  44862  aibandbiaiffaiffb  47963  aibandbiaiaiffb  47964  afv2orxorb  48297