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  19280  isarchi  33623  axextprim  36281  biimpexp  36297  axextndbi  36382  bj-nnfbit  37492  bj-nnfbid  37493  ifpidg  44332  ifp1bi  44343  ifpbibib  44351  rp-fakeanorass  44354  frege54cor0a  44704  aibandbiaiffaiffb  47783  aibandbiaiaiffb  47784  afv2orxorb  48117