Theorem bicom 211

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

Syntax hints:   ↔ wb 195

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 196

This theorem is referenced by:  bicomd  212  bibi1i  327  bibi1d  332  con2bi  342  ibibr  357  bibif  360  nbbn  372  pm5.17  928  biluk  970  bigolden  972  xorcom  1459  trubifal  1513  exists1  2549  abeq1  2720  ssequn1  3745  axpow3  4772  isocnv  6480  qextlt  11908  qextle  11909  rpnnen2lem12  14793  odd2np1  14903  sumodd  14949  nrmmetd  22189  lgsqrmodndvds  24878  cusgrauvtxb  26024  cvmlift2lem12  30550  nn0prpw  31488  bj-abeq1  31962  tsbi4  33113  bicomdd  33153  ifpbicor  36839  rp-fakeoranass  36878  or3or  37339  3impexpbicom  37706  3impexpbicomVD  38114  nabctnabc  39747