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  1013  bigolden  1028  xorcom  1511  norass  1534  trubifal  1568  hadcoma  1596  eqabcb  2881  pm13.183  3666  ssequn1  4196  ab0w  4385  disj  4456  axpow3  5374  isocnv  7350  qextlt  13242  qextle  13243  rpnnen2lem12  16258  odd2np1  16375  sumodd  16422  nrmmetd  24603  lgsqrmodndvds  27412  eqelbid  32503  mgccnv  32974  cvmlift2lem12  35299  nn0prpw  36306  wl-3xorrot  37460  wl-3xorcoma  37461  tsbi4  38123  bicomdd  38836  onsupmaxb  43228  ifpbicor  43465  rp-fakeoranass  43504  or3or  44013  3impexpbicom  44477  3impexpbicomVD  44855  notbicom  45108  limsupreuz  45693  nabctnabc  46881