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 ⊢ ((𝜑 ↔ 𝜓) ↔ (𝜓 ↔ 𝜑))

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  bicomd  226  bibi1i  341  bibi1d  346  con2bi  356  ibibr  371  bibif  374  nbbnOLD  387  biluk  389  biadan  830  pm5.17  1027  bigolden  1042  xorcom  1541  norass  1564  trubifal  1598  hadcoma  1626  eqabcbw  2843  eqabcb  2909  pm13.183  3632  ssequn1  4145  isocnv  7329  qextlt  13229  qextle  13230  rpnnen2lem12  16281  odd2np1  16399  sumodd  16446  nrmmetd  24700  lgsqrmodndvds  27483  eqelbid  32762  mgccnv  33260  cvmlift2lem12  35739  nn0prpw  36757  wl-3xorrot  38046  wl-3xorcoma  38047  tsbi4  38710  bicomdd  39553  onsupmaxb  43893  ifpbicor  44128  rp-fakeoranass  44167  or3or  44676  3impexpbicom  45116  3impexpbicomVD  45492  notbicom  45810  limsupreuz  46378  nabctnabc  47592