Theorem 3anrot 1117

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 1115	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1116	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3anrev  1118  wefrc  5655  ordelord  6382  f13dfv  7272  fr3nr  7767  omword  8551  nnmcan  8616  modmulconst  16341  ncoprmlnprm  16782  issubmndb  18858  pmtr3ncomlem1  19538  srgrmhm  20299  isphld  21804  ordtbaslem  23345  xmetpsmet  24505  comet  24670  cphassr  25371  srabn  25519  lgsdi  27498  divsclw  28388  colopp  29051  colinearalglem2  29257  umgr2edg1  29561  nb3grpr  29732  nb3grpr2  29733  nb3gr2nb  29734  cplgr3v  29785  frgr3v  30626  dipassr  31198  bnj170  35087  bnj290  35099  bnj545  35283  bnj571  35294  bnj594  35300  brapply  36428  brrestrict  36441  dfrdg4  36443  cgrid2  36495  cgr3permute3  36539  cgr3permute2  36541  cgr3permute4  36542  cgr3permute5  36543  colinearperm1  36554  colinearperm3  36555  colinearperm2  36556  colinearperm4  36557  colinearperm5  36558  colinearxfr  36567  endofsegid  36577  colinbtwnle  36610  broutsideof2  36614  dmncan2  38728  isltrn2N  40894  oeord2com  44038  uunTT1p2  45503  uunT11p1  45505  uunT12p2  45509  uunT12p4  45511  3anidm12p2  45515  uun2221p1  45522  en3lplem2VD  45552  grtriproplem  48704  grtrif1o  48707  idomcanr  49113  lincvalpr  49198  alimp-no-surprise  50559