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  2834  eqabcb  2900  pm13.183  3619  ssequn1  4131  isocnv  7326  qextlt  13302  qextle  13303  rpnnen2lem12  16360  odd2np1  16478  sumodd  16525  nrmmetd  24854  lgsqrmodndvds  27643  eqelbid  33004  mgccnv  33493  cvmlift2lem12  36000  nn0prpw  37033  wl-3xorrot  38320  wl-3xorcoma  38321  tsbi4  38988  bicomdd  39831  onsupmaxb  44184  ifpbicor  44419  rp-fakeoranass  44458  or3or  44967  3impexpbicom  45407  3impexpbicomVD  45783  notbicom  46101  limsupreuz  46669  nabctnabc  47923