Theorem 3anrot 1117

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 1115	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1116	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 278	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

This proof depends on syntax axioms:   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anrev  1118  wefrc  5657  ordelord  6386  f13dfv  7281  fr3nr  7777  omword  8561  nnmcan  8626  modmulconst  16368  ncoprmlnprm  16809  issubmndb  18900  pmtr3ncomlem1  19587  srgrmhm  20348  isphld  21854  ordtbaslem  23395  xmetpsmet  24556  comet  24721  cphassr  25422  srabn  25570  lgsdi  27549  divsclw  28439  colopp  29102  colinearalglem2  29312  umgr2edg1  29619  nb3grpr  29790  nb3grpr2  29791  nb3gr2nb  29792  cplgr3v  29843  frgr3v  30697  dipassr  31269  bnj170  35152  bnj290  35164  bnj545  35348  bnj571  35359  bnj594  35365  brapply  36465  brrestrict  36478  dfrdg4  36480  cgrid2  36532  cgr3permute3  36576  cgr3permute2  36578  cgr3permute4  36579  cgr3permute5  36580  colinearperm1  36591  colinearperm3  36592  colinearperm2  36593  colinearperm4  36594  colinearperm5  36595  colinearxfr  36604  endofsegid  36614  colinbtwnle  36647  broutsideof2  36651  dmncan2  38786  isltrn2N  40952  oeord2com  44096  uunTT1p2  45561  uunT11p1  45563  uunT12p2  45567  uunT12p4  45569  3anidm12p2  45573  uun2221p1  45580  en3lplem2VD  45610  grtriproplem  48762  grtrif1o  48765  idomcanr  49170  lincvalpr  49255  alimp-no-surprise  50616