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  1889  nfbid  1902  sbbi  2307  ralbiim  3093  reu8  3701  dfss2  3929  soeq2  5561  fun11  6574  dffo3  7056  dffo3f  7060  isnsg2  19064  isarchi  33109  axextprim  35661  biimpexp  35677  axextndbi  35765  bj-nnfbit  36713  bj-nnfbid  36714  ifpidg  43453  ifp1bi  43464  ifpbibib  43472  rp-fakeanorass  43475  frege54cor0a  43825  aibandbiaiffaiffb  46868  aibandbiaiaiffb  46869  afv2orxorb  47202