Theorem 3anrot 1098

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

Syntax hints:   ↔ wb 205   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  3anrev  1099  wefrc  5574  ordelord  6273  f13dfv  7127  fr3nr  7600  omword  8363  nnmcan  8427  modmulconst  15925  ncoprmlnprm  16360  issubmndb  18359  pmtr3ncomlem1  18996  srgrmhm  19687  isphld  20771  ordtbaslem  22247  xmetpsmet  23409  comet  23575  cphassr  24281  srabn  24429  lgsdi  26387  colopp  27034  colinearalglem2  27178  umgr2edg1  27481  nb3grpr  27652  nb3grpr2  27653  nb3gr2nb  27654  cplgr3v  27705  frgr3v  28540  dipassr  29109  bnj170  32577  bnj290  32589  bnj545  32775  bnj571  32786  bnj594  32792  brapply  34167  brrestrict  34178  dfrdg4  34180  cgrid2  34232  cgr3permute3  34276  cgr3permute2  34278  cgr3permute4  34279  cgr3permute5  34280  colinearperm1  34291  colinearperm3  34292  colinearperm2  34293  colinearperm4  34294  colinearperm5  34295  colinearxfr  34304  endofsegid  34314  colinbtwnle  34347  broutsideof2  34351  dmncan2  36162  isltrn2N  38061  uunTT1p2  42304  uunT11p1  42306  uunT12p2  42310  uunT12p4  42312  3anidm12p2  42316  uun2221p1  42323  en3lplem2VD  42353  lincvalpr  45647  alimp-no-surprise  46371