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  18708  pmtr3ncomlem1  19379  srgrmhm  20107  isphld  21539  ordtbaslem  23051  xmetpsmet  24212  comet  24377  cphassr  25088  srabn  25236  lgsdi  27221  divsclw  28074  colopp  28672  colinearalglem2  28810  umgr2edg1  29114  nb3grpr  29285  nb3grpr2  29286  nb3gr2nb  29287  cplgr3v  29338  frgr3v  30177  dipassr  30748  bnj170  34661  bnj290  34673  bnj545  34858  bnj571  34869  bnj594  34875  brapply  35899  brrestrict  35910  dfrdg4  35912  cgrid2  35964  cgr3permute3  36008  cgr3permute2  36010  cgr3permute4  36011  cgr3permute5  36012  colinearperm1  36023  colinearperm3  36024  colinearperm2  36025  colinearperm4  36026  colinearperm5  36027  colinearxfr  36036  endofsegid  36046  colinbtwnle  36079  broutsideof2  36083  dmncan2  38044  isltrn2N  40087  oeord2com  43273  uunTT1p2  44757  uunT11p1  44759  uunT12p2  44763  uunT12p4  44765  3anidm12p2  44769  uun2221p1  44776  en3lplem2VD  44806  grtriproplem  47911  grtrif1o  47914  lincvalpr  48380  alimp-no-surprise  49743