Theorem bicom 221

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

Syntax hints:   ↔ wb 205

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

This theorem is referenced by:  bicomd  222  bibi1i  339  bibi1d  344  con2bi  354  ibibr  369  bibif  372  nbbn  385  biluk  387  biadan  818  pm5.17  1011  bigolden  1026  xorcom  1513  xorcomOLD  1514  norass  1539  trubifal  1573  hadcoma  1601  eqabcb  2876  ssequn1  4181  ab0w  4374  disj  4448  axpow3  5367  isocnv  7327  qextlt  13182  qextle  13183  rpnnen2lem12  16168  odd2np1  16284  sumodd  16331  nrmmetd  24083  lgsqrmodndvds  26856  eqelbid  31715  mgccnv  32169  cvmlift2lem12  34305  nn0prpw  35208  wl-3xorrot  36358  wl-3xorcoma  36359  tsbi4  37004  bicomdd  37724  onsupmaxb  41988  ifpbicor  42226  rp-fakeoranass  42265  or3or  42774  3impexpbicom  43240  3impexpbicomVD  43618  notbicom  43860  limsupreuz  44453  nabctnabc  45641  isomuspgrlem2b  46497