Theorem bicom 214

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 213	. 2 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 ↔ 𝜑))
2		bicom1 213	. 2 ⊢ ((𝜓 ↔ 𝜑) → (𝜑 ↔ 𝜓))
3	1, 2	impbii 201	1 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Syntax hints:   ↔ wb 198

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 199

This theorem is referenced by:  bicomd  215  bibi1i  331  bibi1d  336  con2bi  346  ibibr  361  bibif  364  nbbn  376  biluk  378  biadan  806  biadanOLD  807  pm5.17  994  bigolden  1009  xorcom  1491  trubifal  1538  euaeOLD  2693  abeq1  2892  ssequn1  4038  axpow3  5118  isocnv  6904  qextlt  12411  qextle  12412  rpnnen2lem12  15436  odd2np1  15548  sumodd  15597  nrmmetd  22899  lgsqrmodndvds  25643  cvmlift2lem12  32175  nn0prpw  33221  bj-abeq1  33635  tsbi4  34887  bicomdd  35464  ifpbicor  39266  rp-fakeoranass  39305  or3or  39763  3impexpbicom  40261  3impexpbicomVD  40639  limsupreuz  41474  nabctnabc  42622  isomuspgrlem2b  43387