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  1013  xor  1016  dfbi3  1049  ifpdfbi  1070  albiim  1890  nfbid  1903  sbbi  2311  ralbiim  3096  reu8  3689  dfss2  3917  soeq2  5552  fun11  6564  dffo3  7045  dffo3f  7049  isnsg2  19083  isarchi  33213  axextprim  35844  biimpexp  35860  axextndbi  35945  bj-nnfbit  36896  bj-nnfbid  36897  ifpidg  43674  ifp1bi  43685  ifpbibib  43693  rp-fakeanorass  43696  frege54cor0a  44046  aibandbiaiffaiffb  47082  aibandbiaiaiffb  47083  afv2orxorb  47416