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  816  pm5.17  1009  bigolden  1024  xorcom  1509  xorcomOLD  1510  norass  1535  trubifal  1570  hadcoma  1600  abeq1  2873  ssequn1  4114  ab0w  4307  disj  4381  axpow3  5291  isocnv  7201  qextlt  12937  qextle  12938  rpnnen2lem12  15934  odd2np1  16050  sumodd  16097  nrmmetd  23730  lgsqrmodndvds  26501  mgccnv  31277  cvmlift2lem12  33276  xpord3ind  33800  nn0prpw  34512  wl-3xorrot  35648  wl-3xorcoma  35649  tsbi4  36294  bicomdd  36868  ifpbicor  41082  rp-fakeoranass  41121  or3or  41631  3impexpbicom  42099  3impexpbicomVD  42477  limsupreuz  43278  nabctnabc  44426  isomuspgrlem2b  45281