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  5544  ordelord  6208  f13dfv  7025  fr3nr  7488  omword  8190  nnmcan  8254  modmulconst  15635  ncoprmlnprm  16062  issubmndb  17964  pmtr3ncomlem1  18595  srgrmhm  19280  isphld  20792  ordtbaslem  21790  xmetpsmet  22952  comet  23117  cphassr  23810  srabn  23957  lgsdi  25904  colopp  26549  colinearalglem2  26687  umgr2edg1  26987  nb3grpr  27158  nb3grpr2  27159  nb3gr2nb  27160  cplgr3v  27211  frgr3v  28048  dipassr  28617  bnj170  31963  bnj290  31975  bnj545  32162  bnj571  32173  bnj594  32179  brapply  33394  brrestrict  33405  dfrdg4  33407  cgrid2  33459  cgr3permute3  33503  cgr3permute2  33505  cgr3permute4  33506  cgr3permute5  33507  colinearperm1  33518  colinearperm3  33519  colinearperm2  33520  colinearperm4  33521  colinearperm5  33522  colinearxfr  33531  endofsegid  33541  colinbtwnle  33574  broutsideof2  33578  dmncan2  35349  isltrn2N  37250  uunTT1p2  41122  uunT11p1  41124  uunT12p2  41128  uunT12p4  41130  3anidm12p2  41134  uun2221p1  41141  en3lplem2VD  41171  lincvalpr  44466  alimp-no-surprise  44875