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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ 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 209  df-an 400

This theorem is referenced by:  dfbi  479  pm4.71  565  impimprbi  839  pm5.17  1025  xor  1028  dfbi3  1061  ifpdfbi  1082  albiim  1909  nfbid  1922  sbbi  2341  ralbiim  3124  reu8  3696  dfss2  3922  soeq2  5577  fun11  6595  dffo3  7083  dffo3f  7087  isnsg2  19197  isarchi  33362  axextprim  36051  biimpexp  36067  axextndbi  36152  bj-nnfbit  37233  bj-nnfbid  37234  ifpidg  44067  ifp1bi  44078  ifpbibib  44086  rp-fakeanorass  44089  frege54cor0a  44439  aibandbiaiffaiffb  47488  aibandbiaiaiffb  47489  afv2orxorb  47822