Theorem 3anrot 1102

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 1100	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1101	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 209   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  3anrev  1103  wefrc  5530  ordelord  6213  f13dfv  7063  fr3nr  7535  omword  8276  nnmcan  8340  modmulconst  15812  ncoprmlnprm  16247  issubmndb  18186  pmtr3ncomlem1  18819  srgrmhm  19505  isphld  20570  ordtbaslem  22039  xmetpsmet  23200  comet  23365  cphassr  24063  srabn  24211  lgsdi  26169  colopp  26814  colinearalglem2  26952  umgr2edg1  27253  nb3grpr  27424  nb3grpr2  27425  nb3gr2nb  27426  cplgr3v  27477  frgr3v  28312  dipassr  28881  bnj170  32343  bnj290  32355  bnj545  32542  bnj571  32553  bnj594  32559  brapply  33926  brrestrict  33937  dfrdg4  33939  cgrid2  33991  cgr3permute3  34035  cgr3permute2  34037  cgr3permute4  34038  cgr3permute5  34039  colinearperm1  34050  colinearperm3  34051  colinearperm2  34052  colinearperm4  34053  colinearperm5  34054  colinearxfr  34063  endofsegid  34073  colinbtwnle  34106  broutsideof2  34110  dmncan2  35921  isltrn2N  37820  uunTT1p2  42029  uunT11p1  42031  uunT12p2  42035  uunT12p4  42037  3anidm12p2  42041  uun2221p1  42048  en3lplem2VD  42078  lincvalpr  45375  alimp-no-surprise  46099