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  5648  ordelord  6374  f13dfv  7266  fr3nr  7764  omword  8580  nnmcan  8644  modmulconst  16305  ncoprmlnprm  16745  issubmndb  18781  pmtr3ncomlem1  19452  srgrmhm  20180  isphld  21612  ordtbaslem  23124  xmetpsmet  24285  comet  24450  cphassr  25162  srabn  25310  lgsdi  27295  divsclw  28137  colopp  28694  colinearalglem2  28832  umgr2edg1  29136  nb3grpr  29307  nb3grpr2  29308  nb3gr2nb  29309  cplgr3v  29360  frgr3v  30202  dipassr  30773  bnj170  34675  bnj290  34687  bnj545  34872  bnj571  34883  bnj594  34889  brapply  35902  brrestrict  35913  dfrdg4  35915  cgrid2  35967  cgr3permute3  36011  cgr3permute2  36013  cgr3permute4  36014  cgr3permute5  36015  colinearperm1  36026  colinearperm3  36027  colinearperm2  36028  colinearperm4  36029  colinearperm5  36030  colinearxfr  36039  endofsegid  36049  colinbtwnle  36082  broutsideof2  36086  dmncan2  38047  isltrn2N  40085  oeord2com  43282  uunTT1p2  44767  uunT11p1  44769  uunT12p2  44773  uunT12p4  44775  3anidm12p2  44779  uun2221p1  44786  en3lplem2VD  44816  grtriproplem  47899  grtrif1o  47902  lincvalpr  48342  alimp-no-surprise  49593