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  817  pm5.17  1010  bigolden  1025  xorcom  1512  xorcomOLD  1513  norass  1538  trubifal  1572  hadcoma  1600  eqabcb  2875  ssequn1  4179  ab0w  4372  disj  4446  axpow3  5365  isocnv  7323  qextlt  13178  qextle  13179  rpnnen2lem12  16164  odd2np1  16280  sumodd  16327  nrmmetd  24074  lgsqrmodndvds  26845  eqelbid  31702  mgccnv  32156  cvmlift2lem12  34293  nn0prpw  35196  wl-3xorrot  36346  wl-3xorcoma  36347  tsbi4  36992  bicomdd  37712  onsupmaxb  41973  ifpbicor  42211  rp-fakeoranass  42250  or3or  42759  3impexpbicom  43225  3impexpbicomVD  43603  notbicom  43845  limsupreuz  44439  nabctnabc  45627  isomuspgrlem2b  46483