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  2809  eqabcb  2875  pm13.183  3619  ssequn1  4137  isocnv  7276  qextlt  13120  qextle  13121  rpnnen2lem12  16152  odd2np1  16270  sumodd  16317  nrmmetd  24520  lgsqrmodndvds  27322  eqelbid  32529  mgccnv  33060  cvmlift2lem12  35487  nn0prpw  36496  wl-3xorrot  37651  wl-3xorcoma  37652  tsbi4  38306  bicomdd  39149  onsupmaxb  43518  ifpbicor  43753  rp-fakeoranass  43792  or3or  44301  3impexpbicom  44758  3impexpbicomVD  45134  notbicom  45446  limsupreuz  46018  nabctnabc  47214