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  338  bibi1d  343  con2bi  353  ibibr  368  bibif  371  nbbn  384  biluk  386  biadan  815  pm5.17  1008  bigolden  1023  xorcom  1506  xorcomOLD  1507  norass  1535  trubifal  1570  hadcoma  1601  abeq1  2872  ssequn1  4110  ab0w  4304  disj  4378  axpow3  5286  isocnv  7181  qextlt  12866  qextle  12867  rpnnen2lem12  15862  odd2np1  15978  sumodd  16025  nrmmetd  23636  lgsqrmodndvds  26406  mgccnv  31179  cvmlift2lem12  33176  xpord3ind  33727  nn0prpw  34439  wl-3xorrot  35575  wl-3xorcoma  35576  tsbi4  36221  bicomdd  36795  ifpbicor  40980  rp-fakeoranass  41019  or3or  41520  3impexpbicom  41988  3impexpbicomVD  42366  limsupreuz  43168  nabctnabc  44313  isomuspgrlem2b  45169