Theorem dfbi2 474

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 213	. 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
2		df-an 396	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
3	1, 2	bitr4i 278	1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  dfbi  475  pm4.71  557  impimprbi  828  pm5.17  1012  xor  1015  dfbi3  1050  ifpdfbi  1071  albiim  1888  nfbid  1901  sbbi  2312  ralbiim  3119  reu8  3755  dfss2  3994  sseq2  4035  soeq2  5630  fun11  6652  dffo3  7136  dffo3f  7140  isnsg2  19196  isarchi  33162  axextprim  35663  biimpexp  35679  axextndbi  35768  bj-nnfbit  36718  bj-nnfbid  36719  ifpidg  43453  ifp1bi  43464  ifpbibib  43472  rp-fakeanorass  43475  frege54cor0a  43825  aibandbiaiffaiffb  46809  aibandbiaiaiffb  46810  afv2orxorb  47143