Theorem dfbi2 478

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

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

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 400

This theorem is referenced by:  dfbi  479  pm4.71  561  impimprbi  829  pm5.17  1012  xor  1015  dfbi3  1050  ifpdfbi  1071  norassOLD  1540  albiim  1897  nfbid  1910  sbbi  2311  ralbiim  3086  reu8  3635  sseq2  3913  soeq2  5475  fun11  6432  dffo3  6899  isnsg2  18526  isarchi  31109  axextprim  33309  biimpexp  33328  axextndbi  33450  bj-nnfbit  34620  bj-nnfbid  34621  andiff  39822  ifpidg  40724  ifp1bi  40735  ifpbibib  40743  rp-fakeanorass  40746  frege54cor0a  41089  dffo3f  42331  aibandbiaiffaiffb  44004  aibandbiaiaiffb  44005  afv2orxorb  44335