Theorem 3anrot 1099

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

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anrev  1100  wefrc  5632  ordelord  6354  f13dfv  7249  fr3nr  7748  omword  8534  nnmcan  8598  modmulconst  16258  ncoprmlnprm  16698  issubmndb  18732  pmtr3ncomlem1  19403  srgrmhm  20131  isphld  21563  ordtbaslem  23075  xmetpsmet  24236  comet  24401  cphassr  25112  srabn  25260  lgsdi  27245  divsclw  28098  colopp  28696  colinearalglem2  28834  umgr2edg1  29138  nb3grpr  29309  nb3grpr2  29310  nb3gr2nb  29311  cplgr3v  29362  frgr3v  30204  dipassr  30775  bnj170  34688  bnj290  34700  bnj545  34885  bnj571  34896  bnj594  34902  brapply  35926  brrestrict  35937  dfrdg4  35939  cgrid2  35991  cgr3permute3  36035  cgr3permute2  36037  cgr3permute4  36038  cgr3permute5  36039  colinearperm1  36050  colinearperm3  36051  colinearperm2  36052  colinearperm4  36053  colinearperm5  36054  colinearxfr  36063  endofsegid  36073  colinbtwnle  36106  broutsideof2  36110  dmncan2  38071  isltrn2N  40114  oeord2com  43300  uunTT1p2  44784  uunT11p1  44786  uunT12p2  44790  uunT12p4  44792  3anidm12p2  44796  uun2221p1  44803  en3lplem2VD  44833  grtriproplem  47938  grtrif1o  47941  lincvalpr  48407  alimp-no-surprise  49770