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  5618  ordelord  6339  f13dfv  7220  fr3nr  7717  omword  8497  nnmcan  8562  modmulconst  16215  ncoprmlnprm  16655  issubmndb  18730  pmtr3ncomlem1  19402  srgrmhm  20157  isphld  21609  ordtbaslem  23132  xmetpsmet  24292  comet  24457  cphassr  25168  srabn  25316  lgsdi  27301  divsclw  28191  colopp  28841  colinearalglem2  28980  umgr2edg1  29284  nb3grpr  29455  nb3grpr2  29456  nb3gr2nb  29457  cplgr3v  29508  frgr3v  30350  dipassr  30921  bnj170  34854  bnj290  34866  bnj545  35051  bnj571  35062  bnj594  35068  brapply  36130  brrestrict  36143  dfrdg4  36145  cgrid2  36197  cgr3permute3  36241  cgr3permute2  36243  cgr3permute4  36244  cgr3permute5  36245  colinearperm1  36256  colinearperm3  36257  colinearperm2  36258  colinearperm4  36259  colinearperm5  36260  colinearxfr  36269  endofsegid  36279  colinbtwnle  36312  broutsideof2  36316  dmncan2  38278  isltrn2N  40380  oeord2com  43553  uunTT1p2  45035  uunT11p1  45037  uunT12p2  45041  uunT12p4  45043  3anidm12p2  45047  uun2221p1  45054  en3lplem2VD  45084  grtriproplem  48185  grtrif1o  48188  lincvalpr  48664  alimp-no-surprise  50026