Theorem dfbi2 658

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  dfbi  659  pm4.71  660  pm5.17  928  xor  931  albiim  1806  nfbid  1820  nfbidOLD  2230  sbbi  2389  ralbiim  3051  reu8  3369  sseq2  3590  soeq2  4979  fun11  5877  dffo3  6282  isnsg2  17447  isarchi  29067  axextprim  30832  biimpexp  30852  axextndbi  30954  ifpdfbi  36837  ifpidg  36855  ifp1bi  36866  ifpbibib  36874  rp-fakeanorass  36877  frege54cor0a  37177  dffo3f  38359  aibandbiaiffaiffb  39710  aibandbiaiaiffb  39711