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  1543  norass  1566  trubifal  1600  hadcoma  1628  eqabcbw  2834  eqabcb  2900  pm13.183  3619  ssequn1  4184  isocnv  7338  qextlt  13333  qextle  13334  rpnnen2lem12  16393  odd2np1  16511  sumodd  16558  nrmmetd  24893  lgsqrmodndvds  27680  eqelbid  33071  mgccnv  33560  cvmlift2lem12  36079  nn0prpw  37111  wl-3xorrot  38401  wl-3xorcoma  38402  tsbi4  39069  bicomdd  39912  onsupmaxb  44241  ifpbicor  44476  rp-fakeoranass  44515  or3or  45023  3impexpbicom  45463  3impexpbicomVD  45839  notbicom  46180  limsupreuz  46747  nabctnabc  48001