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  5652  ordelord  6410  f13dfv  7313  fr3nr  7818  omword  8616  nnmcan  8681  modmulconst  16502  ncoprmlnprm  16948  issubmndb  19050  pmtr3ncomlem1  19738  srgrmhm  20499  isphld  22015  ordtbaslem  23561  xmetpsmet  24722  comet  24887  cphassr  25588  srabn  25736  lgsdi  27718  divsclw  28638  colopp  29304  colinearalglem2  29542  umgr2edg1  29849  nb3grpr  30020  nb3grpr2  30021  nb3gr2nb  30022  cplgr3v  30073  frgr3v  30933  dipassr  31505  bnj170  35440  bnj290  35452  bnj545  35636  bnj571  35647  bnj594  35653  brapply  36915  brrestrict  36928  dfrdg4  36930  cgrid2  36983  cgr3permute3  37027  cgr3permute2  37029  cgr3permute4  37030  cgr3permute5  37031  colinearperm1  37042  colinearperm3  37043  colinearperm2  37044  colinearperm4  37045  colinearperm5  37046  colinearxfr  37055  endofsegid  37065  colinbtwnle  37098  broutsideof2  37102  dmncan2  39277  isltrn2N  41443  oeord2com  44574  uunTT1p2  46037  uunT11p1  46039  uunT12p2  46043  uunT12p4  46045  3anidm12p2  46049  uun2221p1  46056  en3lplem2VD  46086  grtriproplem  49310  grtrif1o  49313  idomcanr  49776  lincvalpr  49861  alimp-no-surprise  51305