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  826  pm5.17  1009  xor  1012  dfbi3  1047  ifpdfbi  1068  albiim  1891  nfbid  1904  sbbi  2304  ralbiim  3113  reu8  3678  sseq2  3957  soeq2  5543  fun11  6545  dffo3  7018  isnsg2  18860  isarchi  31571  axextprim  33781  biimpexp  33797  axextndbi  33911  bj-nnfbit  35008  bj-nnfbid  35009  andiff  40383  ifpidg  41332  ifp1bi  41343  ifpbibib  41351  rp-fakeanorass  41354  frege54cor0a  41705  dffo3f  42958  aibandbiaiffaiffb  44654  aibandbiaiaiffb  44655  afv2orxorb  44985