Theorem 3anrot 1115

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 1113	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1114	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  3anrev  1116  wefrc  5656  ordelord  6383  f13dfv  7273  fr3nr  7770  omword  8554  nnmcan  8619  modmulconst  16345  ncoprmlnprm  16786  issubmndb  18862  pmtr3ncomlem1  19542  srgrmhm  20303  isphld  21772  ordtbaslem  23313  xmetpsmet  24473  comet  24638  cphassr  25339  srabn  25487  lgsdi  27463  divsclw  28353  colopp  29009  colinearalglem2  29197  umgr2edg1  29501  nb3grpr  29672  nb3grpr2  29673  nb3gr2nb  29674  cplgr3v  29725  frgr3v  30566  dipassr  31138  bnj170  35031  bnj290  35043  bnj545  35227  bnj571  35238  bnj594  35244  brapply  36326  brrestrict  36339  dfrdg4  36341  cgrid2  36393  cgr3permute3  36437  cgr3permute2  36439  cgr3permute4  36440  cgr3permute5  36441  colinearperm1  36452  colinearperm3  36453  colinearperm2  36454  colinearperm4  36455  colinearperm5  36456  colinearxfr  36465  endofsegid  36475  colinbtwnle  36508  broutsideof2  36512  dmncan2  38615  isltrn2N  40783  oeord2com  43929  uunTT1p2  45394  uunT11p1  45396  uunT12p2  45400  uunT12p4  45402  3anidm12p2  45406  uun2221p1  45413  en3lplem2VD  45443  grtriproplem  48592  grtrif1o  48595  lincvalpr  49082  alimp-no-surprise  50443