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  2870  pm13.183  3635  ssequn1  4152  ab0w  4345  disj  4416  isocnv  7308  qextlt  13170  qextle  13171  rpnnen2lem12  16200  odd2np1  16318  sumodd  16365  nrmmetd  24469  lgsqrmodndvds  27271  eqelbid  32411  mgccnv  32932  cvmlift2lem12  35308  nn0prpw  36318  wl-3xorrot  37472  wl-3xorcoma  37473  tsbi4  38137  bicomdd  38854  onsupmaxb  43235  ifpbicor  43471  rp-fakeoranass  43510  or3or  44019  3impexpbicom  44477  3impexpbicomVD  44853  notbicom  45166  limsupreuz  45742  nabctnabc  46936