Theorem 3anrot 1100

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

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anrev  1101  wefrc  5616  ordelord  6337  f13dfv  7220  fr3nr  7717  omword  8496  nnmcan  8561  modmulconst  16246  ncoprmlnprm  16687  issubmndb  18762  pmtr3ncomlem1  19437  srgrmhm  20192  isphld  21642  ordtbaslem  23162  xmetpsmet  24322  comet  24487  cphassr  25188  srabn  25336  lgsdi  27316  divsclw  28206  colopp  28856  colinearalglem2  28995  umgr2edg1  29299  nb3grpr  29470  nb3grpr2  29471  nb3gr2nb  29472  cplgr3v  29523  frgr3v  30365  dipassr  30937  bnj170  34862  bnj290  34874  bnj545  35058  bnj571  35069  bnj594  35075  brapply  36139  brrestrict  36152  dfrdg4  36154  cgrid2  36206  cgr3permute3  36250  cgr3permute2  36252  cgr3permute4  36253  cgr3permute5  36254  colinearperm1  36265  colinearperm3  36266  colinearperm2  36267  colinearperm4  36268  colinearperm5  36269  colinearxfr  36278  endofsegid  36288  colinbtwnle  36321  broutsideof2  36325  dmncan2  38409  isltrn2N  40577  oeord2com  43754  uunTT1p2  45236  uunT11p1  45238  uunT12p2  45242  uunT12p4  45244  3anidm12p2  45248  uun2221p1  45255  en3lplem2VD  45285  grtriproplem  48412  grtrif1o  48415  lincvalpr  48891  alimp-no-surprise  50253