Theorem 3anrot 1100

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 1098	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1099	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  3anrev  1101  wefrc  5632  ordelord  6344  f13dfv  7225  fr3nr  7711  omword  8522  nnmcan  8586  modmulconst  16181  ncoprmlnprm  16614  issubmndb  18630  pmtr3ncomlem1  19269  srgrmhm  19967  isphld  21095  ordtbaslem  22576  xmetpsmet  23738  comet  23906  cphassr  24613  srabn  24761  lgsdi  26719  colopp  27774  colinearalglem2  27919  umgr2edg1  28222  nb3grpr  28393  nb3grpr2  28394  nb3gr2nb  28395  cplgr3v  28446  frgr3v  29282  dipassr  29851  bnj170  33399  bnj290  33411  bnj545  33596  bnj571  33607  bnj594  33613  brapply  34599  brrestrict  34610  dfrdg4  34612  cgrid2  34664  cgr3permute3  34708  cgr3permute2  34710  cgr3permute4  34711  cgr3permute5  34712  colinearperm1  34723  colinearperm3  34724  colinearperm2  34725  colinearperm4  34726  colinearperm5  34727  colinearxfr  34736  endofsegid  34746  colinbtwnle  34779  broutsideof2  34783  dmncan2  36609  isltrn2N  38656  oeord2com  41704  uunTT1p2  43199  uunT11p1  43201  uunT12p2  43205  uunT12p4  43207  3anidm12p2  43211  uun2221p1  43218  en3lplem2VD  43248  lincvalpr  46619  alimp-no-surprise  47348