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  5608  ordelord  6328  f13dfv  7208  fr3nr  7705  omword  8485  nnmcan  8549  modmulconst  16199  ncoprmlnprm  16639  issubmndb  18713  pmtr3ncomlem1  19385  srgrmhm  20140  isphld  21591  ordtbaslem  23103  xmetpsmet  24263  comet  24428  cphassr  25139  srabn  25287  lgsdi  27272  divsclw  28134  colopp  28747  colinearalglem2  28885  umgr2edg1  29189  nb3grpr  29360  nb3grpr2  29361  nb3gr2nb  29362  cplgr3v  29413  frgr3v  30255  dipassr  30826  bnj170  34710  bnj290  34722  bnj545  34907  bnj571  34918  bnj594  34924  brapply  35980  brrestrict  35991  dfrdg4  35993  cgrid2  36045  cgr3permute3  36089  cgr3permute2  36091  cgr3permute4  36092  cgr3permute5  36093  colinearperm1  36104  colinearperm3  36105  colinearperm2  36106  colinearperm4  36107  colinearperm5  36108  colinearxfr  36117  endofsegid  36127  colinbtwnle  36160  broutsideof2  36164  dmncan2  38125  isltrn2N  40167  oeord2com  43352  uunTT1p2  44835  uunT11p1  44837  uunT12p2  44841  uunT12p4  44843  3anidm12p2  44847  uun2221p1  44854  en3lplem2VD  44884  grtriproplem  47978  grtrif1o  47981  lincvalpr  48458  alimp-no-surprise  49821