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  3621  ssequn1  4137  ab0w  4330  disj  4401  isocnv  7267  qextlt  13105  qextle  13106  rpnnen2lem12  16134  odd2np1  16252  sumodd  16299  nrmmetd  24460  lgsqrmodndvds  27262  eqelbid  32423  mgccnv  32950  cvmlift2lem12  35307  nn0prpw  36317  wl-3xorrot  37471  wl-3xorcoma  37472  tsbi4  38136  bicomdd  38853  onsupmaxb  43232  ifpbicor  43468  rp-fakeoranass  43507  or3or  44016  3impexpbicom  44474  3impexpbicomVD  44850  notbicom  45163  limsupreuz  45738  nabctnabc  46935