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  5644  ordelord  6384  f13dfv  7282  fr3nr  7786  omword  8579  nnmcan  8644  modmulconst  16459  ncoprmlnprm  16905  issubmndb  19001  pmtr3ncomlem1  19688  srgrmhm  20449  isphld  21961  ordtbaslem  23507  xmetpsmet  24668  comet  24833  cphassr  25534  srabn  25682  lgsdi  27662  divsclw  28582  colopp  29248  colinearalglem2  29486  umgr2edg1  29793  nb3grpr  29964  nb3grpr2  29965  nb3gr2nb  29966  cplgr3v  30017  frgr3v  30877  dipassr  31449  bnj170  35372  bnj290  35384  bnj545  35568  bnj571  35579  bnj594  35585  brapply  36743  brrestrict  36756  dfrdg4  36758  cgrid2  36811  cgr3permute3  36855  cgr3permute2  36857  cgr3permute4  36858  cgr3permute5  36859  colinearperm1  36870  colinearperm3  36871  colinearperm2  36872  colinearperm4  36873  colinearperm5  36874  colinearxfr  36883  endofsegid  36893  colinbtwnle  36926  broutsideof2  36930  dmncan2  39055  isltrn2N  41221  oeord2com  44357  uunTT1p2  45821  uunT11p1  45823  uunT12p2  45827  uunT12p4  45829  3anidm12p2  45833  uun2221p1  45840  en3lplem2VD  45870  grtriproplem  49081  grtrif1o  49084  idomcanr  49489  lincvalpr  49574  alimp-no-surprise  50921