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

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anrev  1100  wefrc  5584  ordelord  6287  f13dfv  7143  fr3nr  7616  omword  8386  nnmcan  8450  modmulconst  15995  ncoprmlnprm  16430  issubmndb  18442  pmtr3ncomlem1  19079  srgrmhm  19770  isphld  20857  ordtbaslem  22337  xmetpsmet  23499  comet  23667  cphassr  24374  srabn  24522  lgsdi  26480  colopp  27128  colinearalglem2  27273  umgr2edg1  27576  nb3grpr  27747  nb3grpr2  27748  nb3gr2nb  27749  cplgr3v  27800  frgr3v  28635  dipassr  29204  bnj170  32673  bnj290  32685  bnj545  32871  bnj571  32882  bnj594  32888  brapply  34236  brrestrict  34247  dfrdg4  34249  cgrid2  34301  cgr3permute3  34345  cgr3permute2  34347  cgr3permute4  34348  cgr3permute5  34349  colinearperm1  34360  colinearperm3  34361  colinearperm2  34362  colinearperm4  34363  colinearperm5  34364  colinearxfr  34373  endofsegid  34383  colinbtwnle  34416  broutsideof2  34420  dmncan2  36231  isltrn2N  38130  uunTT1p2  42385  uunT11p1  42387  uunT12p2  42391  uunT12p4  42393  3anidm12p2  42397  uun2221p1  42404  en3lplem2VD  42434  lincvalpr  45728  alimp-no-surprise  46454