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  1514  norass  1537  trubifal  1571  hadcoma  1599  eqabcb  2869  pm13.183  3632  ssequn1  4149  ab0w  4342  disj  4413  isocnv  7305  qextlt  13163  qextle  13164  rpnnen2lem12  16193  odd2np1  16311  sumodd  16358  nrmmetd  24462  lgsqrmodndvds  27264  eqelbid  32404  mgccnv  32925  cvmlift2lem12  35301  nn0prpw  36311  wl-3xorrot  37465  wl-3xorcoma  37466  tsbi4  38130  bicomdd  38847  onsupmaxb  43228  ifpbicor  43464  rp-fakeoranass  43503  or3or  44012  3impexpbicom  44470  3impexpbicomVD  44846  notbicom  45159  limsupreuz  45735  nabctnabc  46932