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  819  pm5.17  1014  bigolden  1029  xorcom  1516  norass  1539  trubifal  1573  hadcoma  1601  eqabcbw  2811  eqabcb  2877  pm13.183  3621  ssequn1  4139  isocnv  7278  qextlt  13122  qextle  13123  rpnnen2lem12  16154  odd2np1  16272  sumodd  16319  nrmmetd  24522  lgsqrmodndvds  27324  eqelbid  32552  mgccnv  33083  cvmlift2lem12  35510  nn0prpw  36519  wl-3xorrot  37684  wl-3xorcoma  37685  tsbi4  38339  bicomdd  39182  onsupmaxb  43548  ifpbicor  43783  rp-fakeoranass  43822  or3or  44331  3impexpbicom  44788  3impexpbicomVD  45164  notbicom  45476  limsupreuz  46048  nabctnabc  47244