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  5625  ordelord  6342  f13dfv  7231  fr3nr  7728  omword  8511  nnmcan  8575  modmulconst  16234  ncoprmlnprm  16674  issubmndb  18714  pmtr3ncomlem1  19387  srgrmhm  20142  isphld  21596  ordtbaslem  23108  xmetpsmet  24269  comet  24434  cphassr  25145  srabn  25293  lgsdi  27278  divsclw  28138  colopp  28749  colinearalglem2  28887  umgr2edg1  29191  nb3grpr  29362  nb3grpr2  29363  nb3gr2nb  29364  cplgr3v  29415  frgr3v  30254  dipassr  30825  bnj170  34681  bnj290  34693  bnj545  34878  bnj571  34889  bnj594  34895  brapply  35919  brrestrict  35930  dfrdg4  35932  cgrid2  35984  cgr3permute3  36028  cgr3permute2  36030  cgr3permute4  36031  cgr3permute5  36032  colinearperm1  36043  colinearperm3  36044  colinearperm2  36045  colinearperm4  36046  colinearperm5  36047  colinearxfr  36056  endofsegid  36066  colinbtwnle  36099  broutsideof2  36103  dmncan2  38064  isltrn2N  40107  oeord2com  43293  uunTT1p2  44777  uunT11p1  44779  uunT12p2  44783  uunT12p4  44785  3anidm12p2  44789  uun2221p1  44796  en3lplem2VD  44826  grtriproplem  47931  grtrif1o  47934  lincvalpr  48400  alimp-no-surprise  49763