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  5645  ordelord  6387  f13dfv  7286  fr3nr  7790  omword  8586  nnmcan  8651  modmulconst  16467  ncoprmlnprm  16913  issubmndb  19009  pmtr3ncomlem1  19696  srgrmhm  20457  isphld  21969  ordtbaslem  23515  xmetpsmet  24676  comet  24841  cphassr  25542  srabn  25690  lgsdi  27670  divsclw  28590  colopp  29256  colinearalglem2  29494  umgr2edg1  29801  nb3grpr  29972  nb3grpr2  29973  nb3gr2nb  29974  cplgr3v  30025  frgr3v  30885  dipassr  31457  bnj170  35379  bnj290  35391  bnj545  35575  bnj571  35586  bnj594  35592  brapply  36824  brrestrict  36837  dfrdg4  36839  cgrid2  36892  cgr3permute3  36936  cgr3permute2  36938  cgr3permute4  36939  cgr3permute5  36940  colinearperm1  36951  colinearperm3  36952  colinearperm2  36953  colinearperm4  36954  colinearperm5  36955  colinearxfr  36964  endofsegid  36974  colinbtwnle  37007  broutsideof2  37011  dmncan2  39148  isltrn2N  41314  oeord2com  44450  uunTT1p2  45913  uunT11p1  45915  uunT12p2  45919  uunT12p4  45921  3anidm12p2  45925  uun2221p1  45932  en3lplem2VD  45962  grtriproplem  49173  grtrif1o  49176  idomcanr  49581  lincvalpr  49666  alimp-no-surprise  51088