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

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anrev  1118  wefrc  5649  ordelord  6379  f13dfv  7275  fr3nr  7771  omword  8557  nnmcan  8622  modmulconst  16378  ncoprmlnprm  16819  issubmndb  18913  pmtr3ncomlem1  19600  srgrmhm  20361  isphld  21867  ordtbaslem  23413  xmetpsmet  24574  comet  24739  cphassr  25440  srabn  25588  lgsdi  27570  divsclw  28460  colopp  29126  colinearalglem2  29364  umgr2edg1  29671  nb3grpr  29842  nb3grpr2  29843  nb3gr2nb  29844  cplgr3v  29895  frgr3v  30755  dipassr  31327  bnj170  35208  bnj290  35220  bnj545  35404  bnj571  35415  bnj594  35421  brapply  36515  brrestrict  36528  dfrdg4  36530  cgrid2  36583  cgr3permute3  36627  cgr3permute2  36629  cgr3permute4  36630  cgr3permute5  36631  colinearperm1  36642  colinearperm3  36643  colinearperm2  36644  colinearperm4  36645  colinearperm5  36646  colinearxfr  36655  endofsegid  36665  colinbtwnle  36698  broutsideof2  36702  dmncan2  38827  isltrn2N  40993  oeord2com  44152  uunTT1p2  45617  uunT11p1  45619  uunT12p2  45623  uunT12p4  45625  3anidm12p2  45629  uun2221p1  45636  en3lplem2VD  45666  grtriproplem  48855  grtrif1o  48858  idomcanr  49263  lincvalpr  49348  alimp-no-surprise  50710