Theorem dfbi2 476

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  dfbi  477  pm4.71  559  impimprbi  828  pm5.17  1011  xor  1014  dfbi3  1049  ifpdfbi  1070  albiim  1893  nfbid  1906  sbbi  2305  ralbiim  3114  reu8  3730  sseq2  4009  soeq2  5611  fun11  6623  dffo3  7104  isnsg2  19036  isarchi  32328  axextprim  34670  biimpexp  34686  axextndbi  34776  bj-nnfbit  35630  bj-nnfbid  35631  andiff  41019  ifpidg  42242  ifp1bi  42253  ifpbibib  42261  rp-fakeanorass  42264  frege54cor0a  42614  dffo3f  43877  aibandbiaiffaiffb  45604  aibandbiaiaiffb  45605  afv2orxorb  45936