Theorem 3anrot 1101

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 1099	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1100	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ w3a 1088

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 398  df-3an 1090

This theorem is referenced by:  3anrev  1102  wefrc  5671  ordelord  6387  f13dfv  7272  fr3nr  7759  omword  8570  nnmcan  8634  modmulconst  16231  ncoprmlnprm  16664  issubmndb  18686  pmtr3ncomlem1  19341  srgrmhm  20045  isphld  21207  ordtbaslem  22692  xmetpsmet  23854  comet  24022  cphassr  24729  srabn  24877  lgsdi  26837  divsclw  27645  colopp  28051  colinearalglem2  28196  umgr2edg1  28499  nb3grpr  28670  nb3grpr2  28671  nb3gr2nb  28672  cplgr3v  28723  frgr3v  29559  dipassr  30130  bnj170  33740  bnj290  33752  bnj545  33937  bnj571  33948  bnj594  33954  brapply  34941  brrestrict  34952  dfrdg4  34954  cgrid2  35006  cgr3permute3  35050  cgr3permute2  35052  cgr3permute4  35053  cgr3permute5  35054  colinearperm1  35065  colinearperm3  35066  colinearperm2  35067  colinearperm4  35068  colinearperm5  35069  colinearxfr  35078  endofsegid  35088  colinbtwnle  35121  broutsideof2  35125  dmncan2  36993  isltrn2N  39039  oeord2com  42109  uunTT1p2  43604  uunT11p1  43606  uunT12p2  43610  uunT12p4  43612  3anidm12p2  43616  uun2221p1  43623  en3lplem2VD  43653  lincvalpr  47147  alimp-no-surprise  47876