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  1014  bigolden  1029  xorcom  1516  norass  1539  trubifal  1573  hadcoma  1601  eqabcbw  2810  eqabcb  2876  pm13.183  3608  ssequn1  4126  isocnv  7285  qextlt  13155  qextle  13156  rpnnen2lem12  16192  odd2np1  16310  sumodd  16357  nrmmetd  24539  lgsqrmodndvds  27316  eqelbid  32544  mgccnv  33059  cvmlift2lem12  35496  nn0prpw  36505  wl-3xorrot  37793  wl-3xorcoma  37794  tsbi4  38457  bicomdd  39300  onsupmaxb  43667  ifpbicor  43902  rp-fakeoranass  43941  or3or  44450  3impexpbicom  44907  3impexpbicomVD  45283  notbicom  45595  limsupreuz  46165  nabctnabc  47379