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  340  bibi1d  345  con2bi  355  ibibr  370  bibif  373  nbbn  385  biluk  387  biadan  825  pm5.17  1020  bigolden  1035  xorcom  1522  norass  1545  trubifal  1579  hadcoma  1607  eqabcbw  2815  eqabcb  2881  pm13.183  3606  ssequn1  4118  isocnv  7278  qextlt  13150  qextle  13151  rpnnen2lem12  16187  odd2np1  16305  sumodd  16352  nrmmetd  24561  lgsqrmodndvds  27338  eqelbid  32566  mgccnv  33082  cvmlift2lem12  35557  nn0prpw  36566  wl-3xorrot  37854  wl-3xorcoma  37855  tsbi4  38518  bicomdd  39361  onsupmaxb  43699  ifpbicor  43934  rp-fakeoranass  43973  or3or  44482  3impexpbicom  44939  3impexpbicomVD  45315  notbicom  45626  limsupreuz  46194  nabctnabc  47408