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  norassOLD  1536  albiim  1892  nfbid  1905  sbbi  2305  ralbiim  3099  reu8  3668  sseq2  3947  soeq2  5525  fun11  6508  dffo3  6978  isnsg2  18784  isarchi  31436  axextprim  33642  biimpexp  33659  axextndbi  33780  bj-nnfbit  34934  bj-nnfbid  34935  andiff  40159  ifpidg  41098  ifp1bi  41109  ifpbibib  41117  rp-fakeanorass  41120  frege54cor0a  41471  dffo3f  42717  aibandbiaiffaiffb  44389  aibandbiaiaiffb  44390  afv2orxorb  44720