Theorem dfbi2 462

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 197   ∧ wa 384

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 198  df-an 385

This theorem is referenced by:  dfbi  463  pm4.71  549  pm5.17  1026  xor  1029  dfbi3  1063  albiim  1978  nfbid  1994  nfbidOLD  2416  sbbi  2560  ralbiim  3257  reu8  3600  sseq2  3824  soeq2  5252  fun11  6174  dffo3  6596  isnsg2  17826  isarchi  30061  axextprim  31900  biimpexp  31919  axextndbi  32030  ifpdfbi  38318  ifpidg  38336  ifp1bi  38347  ifpbibib  38355  rp-fakeanorass  38358  frege54cor0a  38657  dffo3f  39853  aibandbiaiffaiffb  41543  aibandbiaiaiffb  41544  afv2orxorb  41817