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  3620  ssequn1  4132  isocnv  7331  qextlt  13255  qextle  13256  rpnnen2lem12  16313  odd2np1  16431  sumodd  16478  nrmmetd  24800  lgsqrmodndvds  27589  eqelbid  32950  mgccnv  33439  cvmlift2lem12  35893  nn0prpw  36942  wl-3xorrot  38231  wl-3xorcoma  38232  tsbi4  38884  bicomdd  39727  onsupmaxb  44080  ifpbicor  44315  rp-fakeoranass  44354  or3or  44863  3impexpbicom  45303  3impexpbicomVD  45679  notbicom  45997  limsupreuz  46565  nabctnabc  47819