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  5682  ordelord  6407  f13dfv  7293  fr3nr  7790  omword  8606  nnmcan  8670  modmulconst  16321  ncoprmlnprm  16761  issubmndb  18830  pmtr3ncomlem1  19505  srgrmhm  20239  isphld  21689  ordtbaslem  23211  xmetpsmet  24373  comet  24541  cphassr  25259  srabn  25407  lgsdi  27392  divsclw  28234  colopp  28791  colinearalglem2  28936  umgr2edg1  29242  nb3grpr  29413  nb3grpr2  29414  nb3gr2nb  29415  cplgr3v  29466  frgr3v  30303  dipassr  30874  bnj170  34690  bnj290  34702  bnj545  34887  bnj571  34898  bnj594  34904  brapply  35919  brrestrict  35930  dfrdg4  35932  cgrid2  35984  cgr3permute3  36028  cgr3permute2  36030  cgr3permute4  36031  cgr3permute5  36032  colinearperm1  36043  colinearperm3  36044  colinearperm2  36045  colinearperm4  36046  colinearperm5  36047  colinearxfr  36056  endofsegid  36066  colinbtwnle  36099  broutsideof2  36103  dmncan2  38063  isltrn2N  40102  oeord2com  43300  uunTT1p2  44792  uunT11p1  44794  uunT12p2  44798  uunT12p4  44800  3anidm12p2  44804  uun2221p1  44811  en3lplem2VD  44841  grtriproplem  47843  grtrif1o  47846  lincvalpr  48263  alimp-no-surprise  49011