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  2876  pm13.183  3645  ssequn1  4161  ab0w  4354  disj  4425  isocnv  7323  qextlt  13219  qextle  13220  rpnnen2lem12  16243  odd2np1  16360  sumodd  16407  nrmmetd  24513  lgsqrmodndvds  27316  eqelbid  32456  mgccnv  32979  cvmlift2lem12  35336  nn0prpw  36341  wl-3xorrot  37495  wl-3xorcoma  37496  tsbi4  38160  bicomdd  38872  onsupmaxb  43263  ifpbicor  43499  rp-fakeoranass  43538  or3or  44047  3impexpbicom  44505  3impexpbicomVD  44881  notbicom  45189  limsupreuz  45766  nabctnabc  46960