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  5635  ordelord  6357  f13dfv  7252  fr3nr  7751  omword  8537  nnmcan  8601  modmulconst  16265  ncoprmlnprm  16705  issubmndb  18739  pmtr3ncomlem1  19410  srgrmhm  20138  isphld  21570  ordtbaslem  23082  xmetpsmet  24243  comet  24408  cphassr  25119  srabn  25267  lgsdi  27252  divsclw  28105  colopp  28703  colinearalglem2  28841  umgr2edg1  29145  nb3grpr  29316  nb3grpr2  29317  nb3gr2nb  29318  cplgr3v  29369  frgr3v  30211  dipassr  30782  bnj170  34695  bnj290  34707  bnj545  34892  bnj571  34903  bnj594  34909  brapply  35933  brrestrict  35944  dfrdg4  35946  cgrid2  35998  cgr3permute3  36042  cgr3permute2  36044  cgr3permute4  36045  cgr3permute5  36046  colinearperm1  36057  colinearperm3  36058  colinearperm2  36059  colinearperm4  36060  colinearperm5  36061  colinearxfr  36070  endofsegid  36080  colinbtwnle  36113  broutsideof2  36117  dmncan2  38078  isltrn2N  40121  oeord2com  43307  uunTT1p2  44791  uunT11p1  44793  uunT12p2  44797  uunT12p4  44799  3anidm12p2  44803  uun2221p1  44810  en3lplem2VD  44840  grtriproplem  47942  grtrif1o  47945  lincvalpr  48411  alimp-no-surprise  49774