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  829  pm5.17  1014  xor  1017  dfbi3  1050  ifpdfbi  1071  albiim  1889  nfbid  1902  sbbi  2308  ralbiim  3113  reu8  3739  dfss2  3969  soeq2  5614  fun11  6640  dffo3  7122  dffo3f  7126  isnsg2  19174  isarchi  33189  axextprim  35701  biimpexp  35717  axextndbi  35805  bj-nnfbit  36753  bj-nnfbid  36754  ifpidg  43504  ifp1bi  43515  ifpbibib  43523  rp-fakeanorass  43526  frege54cor0a  43876  aibandbiaiffaiffb  46906  aibandbiaiaiffb  46907  afv2orxorb  47240