Theorem 3anrot 1096

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

Syntax hints:   ↔ wb 208   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  3anrev  1097  wefrc  5551  ordelord  6215  f13dfv  7033  fr3nr  7496  omword  8198  nnmcan  8262  modmulconst  15643  ncoprmlnprm  16070  issubmndb  17972  pmtr3ncomlem1  18603  srgrmhm  19288  isphld  20800  ordtbaslem  21798  xmetpsmet  22960  comet  23125  cphassr  23818  srabn  23965  lgsdi  25912  colopp  26557  colinearalglem2  26695  umgr2edg1  26995  nb3grpr  27166  nb3grpr2  27167  nb3gr2nb  27168  cplgr3v  27219  frgr3v  28056  dipassr  28625  bnj170  31970  bnj290  31982  bnj545  32169  bnj571  32180  bnj594  32186  brapply  33401  brrestrict  33412  dfrdg4  33414  cgrid2  33466  cgr3permute3  33510  cgr3permute2  33512  cgr3permute4  33513  cgr3permute5  33514  colinearperm1  33525  colinearperm3  33526  colinearperm2  33527  colinearperm4  33528  colinearperm5  33529  colinearxfr  33538  endofsegid  33548  colinbtwnle  33581  broutsideof2  33585  dmncan2  35357  isltrn2N  37258  uunTT1p2  41136  uunT11p1  41138  uunT12p2  41142  uunT12p4  41144  3anidm12p2  41148  uun2221p1  41155  en3lplem2VD  41185  lincvalpr  44480  alimp-no-surprise  44889