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  1013  bigolden  1028  xorcom  1515  norass  1538  trubifal  1572  hadcoma  1600  eqabcbw  2805  eqabcb  2872  pm13.183  3616  ssequn1  4133  isocnv  7264  qextlt  13102  qextle  13103  rpnnen2lem12  16134  odd2np1  16252  sumodd  16299  nrmmetd  24489  lgsqrmodndvds  27291  eqelbid  32454  mgccnv  32980  cvmlift2lem12  35358  nn0prpw  36367  wl-3xorrot  37521  wl-3xorcoma  37522  tsbi4  38175  bicomdd  38952  onsupmaxb  43331  ifpbicor  43567  rp-fakeoranass  43606  or3or  44115  3impexpbicom  44572  3impexpbicomVD  44948  notbicom  45261  limsupreuz  45834  nabctnabc  47030