Theorem bicom 225

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bicomd  226  bibi1i  341  bibi1d  346  con2bi  356  ibibr  371  bibif  374  nbbnOLD  387  birot  389  biluk  390  biadan  831  pm5.17  1029  bigolden  1044  xorcom  1544  norass  1567  trubifal  1601  hadcoma  1629  eqabcbw  2836  eqabcb  2902  pm13.183  3623  ssequn1  4135  isocnv  7334  qextlt  13257  qextle  13258  rpnnen2lem12  16317  odd2np1  16435  sumodd  16482  nrmmetd  24801  lgsqrmodndvds  27587  eqelbid  32936  mgccnv  33426  cvmlift2lem12  35880  nn0prpw  36929  wl-3xorrot  38218  wl-3xorcoma  38219  tsbi4  38871  bicomdd  39714  onsupmaxb  44067  ifpbicor  44302  rp-fakeoranass  44341  or3or  44850  3impexpbicom  45290  3impexpbicomVD  45666  notbicom  45984  limsupreuz  46552  nabctnabc  47806