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  5645  ordelord  6384  f13dfv  7282  fr3nr  7786  omword  8578  nnmcan  8643  modmulconst  16458  ncoprmlnprm  16904  issubmndb  19000  pmtr3ncomlem1  19687  srgrmhm  20448  isphld  21960  ordtbaslem  23506  xmetpsmet  24667  comet  24832  cphassr  25533  srabn  25681  lgsdi  27661  divsclw  28581  colopp  29247  colinearalglem2  29485  umgr2edg1  29792  nb3grpr  29963  nb3grpr2  29964  nb3gr2nb  29965  cplgr3v  30016  frgr3v  30876  dipassr  31448  bnj170  35329  bnj290  35341  bnj545  35525  bnj571  35536  bnj594  35542  brapply  36700  brrestrict  36713  dfrdg4  36715  cgrid2  36768  cgr3permute3  36812  cgr3permute2  36814  cgr3permute4  36815  cgr3permute5  36816  colinearperm1  36827  colinearperm3  36828  colinearperm2  36829  colinearperm4  36830  colinearperm5  36831  colinearxfr  36840  endofsegid  36850  colinbtwnle  36883  broutsideof2  36887  dmncan2  39011  isltrn2N  41177  oeord2com  44312  uunTT1p2  45776  uunT11p1  45778  uunT12p2  45782  uunT12p4  45784  3anidm12p2  45788  uun2221p1  45795  en3lplem2VD  45825  grtriproplem  49036  grtrif1o  49039  idomcanr  49444  lincvalpr  49529  alimp-no-surprise  50876