Theorem bicom 224

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  bicomd  225  bibi1i  341  bibi1d  346  con2bi  356  ibibr  371  bibif  374  nbbn  387  biluk  389  biadan  817  pm5.17  1008  bigolden  1023  xorcom  1503  norass  1529  trubifal  1564  hadcoma  1595  abeq1  2946  ssequn1  4155  axpow3  5261  isocnv  7077  qextlt  12590  qextle  12591  rpnnen2lem12  15572  odd2np1  15684  sumodd  15733  nrmmetd  23178  lgsqrmodndvds  25923  cvmlift2lem12  32556  nn0prpw  33666  tsbi4  35408  bicomdd  35984  ifpbicor  39834  rp-fakeoranass  39873  or3or  40364  3impexpbicom  40806  3impexpbicomVD  41184  limsupreuz  42011  nabctnabc  43161  isomuspgrlem2b  43988