Theorem dfbi2 475

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

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

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 397

This theorem is referenced by:  dfbi  476  pm4.71  558  impimprbi  827  pm5.17  1010  xor  1013  dfbi3  1048  ifpdfbi  1069  albiim  1892  nfbid  1905  sbbi  2304  ralbiim  3112  reu8  3694  sseq2  3973  soeq2  5572  fun11  6580  dffo3  7057  isnsg2  18972  isarchi  32088  axextprim  34359  biimpexp  34375  axextndbi  34465  bj-nnfbit  35293  bj-nnfbid  35294  andiff  40684  ifpidg  41885  ifp1bi  41896  ifpbibib  41904  rp-fakeanorass  41907  frege54cor0a  42257  dffo3f  43520  aibandbiaiffaiffb  45249  aibandbiaiaiffb  45250  afv2orxorb  45580