Theorem 3anrot 1099

Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.) (Proof shortened by Wolf Lammen, 9-Jun-2022.)

Assertion

Ref	Expression
3anrot	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Proof of Theorem 3anrot

Step	Hyp	Ref	Expression
1		3ancoma 1097	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1098	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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  df-an 396  df-3an 1088

This theorem is referenced by:  3anrev  1100  wefrc  5616  ordelord  6337  f13dfv  7218  fr3nr  7715  omword  8495  nnmcan  8560  modmulconst  16213  ncoprmlnprm  16653  issubmndb  18728  pmtr3ncomlem1  19400  srgrmhm  20155  isphld  21607  ordtbaslem  23130  xmetpsmet  24290  comet  24455  cphassr  25166  srabn  25314  lgsdi  27299  divsclw  28164  colopp  28790  colinearalglem2  28929  umgr2edg1  29233  nb3grpr  29404  nb3grpr2  29405  nb3gr2nb  29406  cplgr3v  29457  frgr3v  30299  dipassr  30870  bnj170  34803  bnj290  34815  bnj545  35000  bnj571  35011  bnj594  35017  brapply  36079  brrestrict  36092  dfrdg4  36094  cgrid2  36146  cgr3permute3  36190  cgr3permute2  36192  cgr3permute4  36193  cgr3permute5  36194  colinearperm1  36205  colinearperm3  36206  colinearperm2  36207  colinearperm4  36208  colinearperm5  36209  colinearxfr  36218  endofsegid  36228  colinbtwnle  36261  broutsideof2  36265  dmncan2  38217  isltrn2N  40319  oeord2com  43495  uunTT1p2  44977  uunT11p1  44979  uunT12p2  44983  uunT12p4  44985  3anidm12p2  44989  uun2221p1  44996  en3lplem2VD  45026  grtriproplem  48127  grtrif1o  48130  lincvalpr  48606  alimp-no-surprise  49968