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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  dfbi  475  pm4.71  557  impimprbi  825  pm5.17  1008  xor  1011  dfbi3  1046  ifpdfbi  1067  norassOLD  1536  albiim  1893  nfbid  1906  sbbi  2308  ralbiim  3098  reu8  3663  sseq2  3943  soeq2  5516  fun11  6492  dffo3  6960  isnsg2  18699  isarchi  31338  axextprim  33542  biimpexp  33561  axextndbi  33686  bj-nnfbit  34861  bj-nnfbid  34862  andiff  40087  ifpidg  40996  ifp1bi  41007  ifpbibib  41015  rp-fakeanorass  41018  frege54cor0a  41360  dffo3f  42606  aibandbiaiffaiffb  44276  aibandbiaiaiffb  44277  afv2orxorb  44607