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 274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anrev  1100  wefrc  5583  ordelord  6288  f13dfv  7146  fr3nr  7622  omword  8401  nnmcan  8465  modmulconst  15997  ncoprmlnprm  16432  issubmndb  18444  pmtr3ncomlem1  19081  srgrmhm  19772  isphld  20859  ordtbaslem  22339  xmetpsmet  23501  comet  23669  cphassr  24376  srabn  24524  lgsdi  26482  colopp  27130  colinearalglem2  27275  umgr2edg1  27578  nb3grpr  27749  nb3grpr2  27750  nb3gr2nb  27751  cplgr3v  27802  frgr3v  28639  dipassr  29208  bnj170  32677  bnj290  32689  bnj545  32875  bnj571  32886  bnj594  32892  brapply  34240  brrestrict  34251  dfrdg4  34253  cgrid2  34305  cgr3permute3  34349  cgr3permute2  34351  cgr3permute4  34352  cgr3permute5  34353  colinearperm1  34364  colinearperm3  34365  colinearperm2  34366  colinearperm4  34367  colinearperm5  34368  colinearxfr  34377  endofsegid  34387  colinbtwnle  34420  broutsideof2  34424  dmncan2  36235  isltrn2N  38134  uunTT1p2  42415  uunT11p1  42417  uunT12p2  42421  uunT12p4  42423  3anidm12p2  42427  uun2221p1  42434  en3lplem2VD  42464  lincvalpr  45759  alimp-no-surprise  46485