Theorem dfbi2 477

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  dfbi  478  pm4.71  560  impimprbi  826  pm5.17  1008  xor  1011  dfbi3  1044  norassOLD  1530  albiim  1886  nfbid  1899  sbbi  2313  sbbivOLD  2323  sbbiALT  2607  ralbiim  3174  reu8  3723  sseq2  3992  soeq2  5489  fun11  6422  dffo3  6862  isnsg2  18302  isarchi  30806  axextprim  32922  biimpexp  32941  axextndbi  33044  bj-nnfbit  34076  bj-nnfbid  34077  andiff  39092  ifpdfbi  39832  ifpidg  39850  ifp1bi  39861  ifpbibib  39869  rp-fakeanorass  39872  frege54cor0a  40202  dffo3f  41431  aibandbiaiffaiffb  43124  aibandbiaiaiffb  43125  afv2orxorb  43421