Theorem dfbi2 475

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 207   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  dfbi  476  pm4.71  562  impimprbi  834  pm5.17  1019  xor  1022  dfbi3  1055  ifpdfbi  1076  albiim  1896  nfbid  1909  sbbi  2318  ralbiim  3101  reu8  3674  dfss2  3901  soeq2  5548  fun11  6559  dffo3  7043  dffo3f  7047  isnsg2  19122  isarchi  33263  axextprim  35929  biimpexp  35945  axextndbi  36030  bj-nnfbit  37101  bj-nnfbid  37102  ifpidg  43935  ifp1bi  43946  ifpbibib  43954  rp-fakeanorass  43957  frege54cor0a  44307  aibandbiaiffaiffb  47357  aibandbiaiaiffb  47358  afv2orxorb  47691