Theorem dfbi2 479

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 401	. 2 ⊢ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
3	1, 2	bitr4i 281	1 ⊢ ((𝜑 ↔ 𝜓) ↔ ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  dfbi  480  pm4.71  566  impimprbi  841  pm5.17  1029  xor  1032  dfbi3  1065  ifpdfbiOLD  1087  albiim  1919  nfbid  1932  sbbi  2342  ralbiim  3127  reu8  3696  dfss2  3923  soeq2  5591  fun11  6610  dffo3  7097  dffo3f  7101  isnsg2  19217  isarchi  33502  axextprim  36193  biimpexp  36209  axextndbi  36294  bj-nnfbit  37403  bj-nnfbid  37404  ifpidg  44237  ifp1bi  44248  ifpbibib  44256  rp-fakeanorass  44259  frege54cor0a  44609  aibandbiaiffaiffb  47651  aibandbiaiaiffb  47652  afv2orxorb  47985