Theorem 3anrot 1100

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 1098	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1099	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anrev  1101  wefrc  5626  ordelord  6347  f13dfv  7230  fr3nr  7727  omword  8507  nnmcan  8572  modmulconst  16227  ncoprmlnprm  16667  issubmndb  18742  pmtr3ncomlem1  19414  srgrmhm  20169  isphld  21621  ordtbaslem  23144  xmetpsmet  24304  comet  24469  cphassr  25180  srabn  25328  lgsdi  27313  divsclw  28203  colopp  28853  colinearalglem2  28992  umgr2edg1  29296  nb3grpr  29467  nb3grpr2  29468  nb3gr2nb  29469  cplgr3v  29520  frgr3v  30362  dipassr  30934  bnj170  34875  bnj290  34887  bnj545  35071  bnj571  35082  bnj594  35088  brapply  36152  brrestrict  36165  dfrdg4  36167  cgrid2  36219  cgr3permute3  36263  cgr3permute2  36265  cgr3permute4  36266  cgr3permute5  36267  colinearperm1  36278  colinearperm3  36279  colinearperm2  36280  colinearperm4  36281  colinearperm5  36282  colinearxfr  36291  endofsegid  36301  colinbtwnle  36334  broutsideof2  36338  dmncan2  38328  isltrn2N  40496  oeord2com  43668  uunTT1p2  45150  uunT11p1  45152  uunT12p2  45156  uunT12p4  45158  3anidm12p2  45162  uun2221p1  45169  en3lplem2VD  45199  grtriproplem  48299  grtrif1o  48302  lincvalpr  48778  alimp-no-surprise  50140