Theorem dfbi2 467

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  dfbi  468  pm4.71  550  pm5.17  994  xor  997  dfbi3  1030  albiim  1852  nfbid  1865  sbbi  2241  sbbivOLD  2250  sbbiALT  2538  eu6OLDOLD  2593  ralbiim  3124  reu8  3636  sseq2  3883  soeq2  5347  fun11  6261  dffo3  6691  isnsg2  18093  isarchi  30483  axextprim  32453  biimpexp  32472  axextndbi  32576  ifpdfbi  39241  ifpidg  39259  ifp1bi  39270  ifpbibib  39278  rp-fakeanorass  39281  frege54cor0a  39578  dffo3f  40868  aibandbiaiffaiffb  42566  aibandbiaiaiffb  42567  afv2orxorb  42839