Theorem 3anrot 1105

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 1103	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1104	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 276	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anrev  1106  wefrc  5612  ordelord  6332  f13dfv  7218  fr3nr  7715  omword  8495  nnmcan  8560  modmulconst  16248  ncoprmlnprm  16689  issubmndb  18764  pmtr3ncomlem1  19439  srgrmhm  20194  isphld  21629  ordtbaslem  23171  xmetpsmet  24331  comet  24496  cphassr  25197  srabn  25345  lgsdi  27315  divsclw  28205  colopp  28855  colinearalglem2  28994  umgr2edg1  29298  nb3grpr  29469  nb3grpr2  29470  nb3gr2nb  29471  cplgr3v  29522  frgr3v  30363  dipassr  30935  bnj170  34881  bnj290  34893  bnj545  35077  bnj571  35088  bnj594  35094  brapply  36164  brrestrict  36177  dfrdg4  36179  cgrid2  36231  cgr3permute3  36275  cgr3permute2  36277  cgr3permute4  36278  cgr3permute5  36279  colinearperm1  36290  colinearperm3  36291  colinearperm2  36292  colinearperm4  36293  colinearperm5  36294  colinearxfr  36303  endofsegid  36313  colinbtwnle  36346  broutsideof2  36350  dmncan2  38444  isltrn2N  40612  oeord2com  43756  uunTT1p2  45238  uunT11p1  45240  uunT12p2  45244  uunT12p4  45246  3anidm12p2  45250  uun2221p1  45257  en3lplem2VD  45287  grtriproplem  48430  grtrif1o  48433  lincvalpr  48909  alimp-no-surprise  50271