Theorem bicom 222

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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bicomd  223  bibi1i  338  bibi1d  343  con2bi  353  ibibr  368  bibif  371  nbbn  383  biluk  385  biadan  819  pm5.17  1014  bigolden  1029  xorcom  1516  norass  1539  trubifal  1573  hadcoma  1601  eqabcbw  2811  eqabcb  2877  pm13.183  3609  ssequn1  4127  isocnv  7280  qextlt  13150  qextle  13151  rpnnen2lem12  16187  odd2np1  16305  sumodd  16352  nrmmetd  24553  lgsqrmodndvds  27334  eqelbid  32563  mgccnv  33078  cvmlift2lem12  35516  nn0prpw  36525  wl-3xorrot  37813  wl-3xorcoma  37814  tsbi4  38477  bicomdd  39320  onsupmaxb  43691  ifpbicor  43926  rp-fakeoranass  43965  or3or  44474  3impexpbicom  44931  3impexpbicomVD  45307  notbicom  45619  limsupreuz  46189  nabctnabc  47397