Theorem 3anrot 1112

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 1110	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1111	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 277	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 208   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3anrev  1113  wefrc  5641  ordelord  6368  f13dfv  7258  fr3nr  7755  omword  8539  nnmcan  8604  modmulconst  16322  ncoprmlnprm  16763  issubmndb  18839  pmtr3ncomlem1  19513  srgrmhm  20268  isphld  21703  ordtbaslem  23245  xmetpsmet  24405  comet  24570  cphassr  25271  srabn  25419  lgsdi  27395  divsclw  28285  colopp  28939  colinearalglem2  29105  umgr2edg1  29409  nb3grpr  29580  nb3grpr2  29581  nb3gr2nb  29582  cplgr3v  29633  frgr3v  30474  dipassr  31046  bnj170  34991  bnj290  35003  bnj545  35187  bnj571  35198  bnj594  35204  brapply  36283  brrestrict  36296  dfrdg4  36298  cgrid2  36350  cgr3permute3  36394  cgr3permute2  36396  cgr3permute4  36397  cgr3permute5  36398  colinearperm1  36409  colinearperm3  36410  colinearperm2  36411  colinearperm4  36412  colinearperm5  36413  colinearxfr  36422  endofsegid  36432  colinbtwnle  36465  broutsideof2  36469  dmncan2  38573  isltrn2N  40741  oeord2com  43885  uunTT1p2  45367  uunT11p1  45369  uunT12p2  45373  uunT12p4  45375  3anidm12p2  45379  uun2221p1  45386  en3lplem2VD  45416  grtriproplem  48558  grtrif1o  48561  lincvalpr  49037  alimp-no-surprise  50399