Theorem bicom 222

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

Syntax hints:   ↔ wb 206

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 207

This theorem is referenced by:  bicomd  223  bibi1i  338  bibi1d  343  con2bi  353  ibibr  368  bibif  371  nbbn  383  biluk  385  biadan  818  pm5.17  1012  bigolden  1027  xorcom  1511  norass  1534  trubifal  1568  hadcoma  1596  eqabcb  2886  pm13.183  3679  ssequn1  4209  ab0w  4401  disj  4473  axpow3  5386  isocnv  7366  qextlt  13265  qextle  13266  rpnnen2lem12  16273  odd2np1  16389  sumodd  16436  nrmmetd  24608  lgsqrmodndvds  27415  eqelbid  32503  mgccnv  32972  cvmlift2lem12  35282  nn0prpw  36289  wl-3xorrot  37443  wl-3xorcoma  37444  tsbi4  38096  bicomdd  38810  onsupmaxb  43200  ifpbicor  43437  rp-fakeoranass  43476  or3or  43985  3impexpbicom  44450  3impexpbicomVD  44828  notbicom  45071  limsupreuz  45658  nabctnabc  46846