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  2344  ralbiim  3129  reu8  3698  dfss2  3924  soeq2  5593  fun11  6614  dffo3  7101  dffo3f  7105  isnsg2  19268  isarchi  33568  axextprim  36232  biimpexp  36248  axextndbi  36333  bj-nnfbit  37442  bj-nnfbid  37443  ifpidg  44277  ifp1bi  44288  ifpbibib  44296  rp-fakeanorass  44299  frege54cor0a  44649  aibandbiaiffaiffb  47691  aibandbiaiaiffb  47692  afv2orxorb  48025