Theorem bicom 225

Description: Commutative law for the biconditional. Theorem *4.21 of [WhiteheadRussell] p. 117. (Contributed by NM, 11-May-1993.)

Assertion

Ref	Expression
bicom	⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Proof of Theorem bicom

Step	Hyp	Ref	Expression
1		bicom1 224	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
2		bicom1 224	. 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
3	1, 2	impbii 212	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bicomd  226  bibi1i  342  bibi1d  347  con2bi  357  ibibr  372  bibif  375  nbbn  388  biluk  390  biadan  818  pm5.17  1009  bigolden  1024  xorcom  1505  xorcomOLD  1506  norass  1534  trubifal  1569  hadcoma  1600  abeq1  2885  ssequn1  4087  disj  4347  axpow3  5240  isocnv  7082  qextlt  12642  qextle  12643  rpnnen2lem12  15631  odd2np1  15747  sumodd  15794  nrmmetd  23281  lgsqrmodndvds  26041  mgccnv  30807  cvmlift2lem12  32796  xpord3ind  33359  nn0prpw  34087  wl-3xorrot  35200  wl-3xorcoma  35201  tsbi4  35880  bicomdd  36456  ifpbicor  40584  rp-fakeoranass  40623  or3or  41125  3impexpbicom  41586  3impexpbicomVD  41964  limsupreuz  42773  nabctnabc  43918  isomuspgrlem2b  44742