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 275	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anrev  1101  wefrc  5694  ordelord  6417  f13dfv  7310  fr3nr  7807  omword  8626  nnmcan  8690  modmulconst  16336  ncoprmlnprm  16775  issubmndb  18840  pmtr3ncomlem1  19515  srgrmhm  20249  isphld  21695  ordtbaslem  23217  xmetpsmet  24379  comet  24547  cphassr  25265  srabn  25413  lgsdi  27396  divsclw  28238  colopp  28795  colinearalglem2  28940  umgr2edg1  29246  nb3grpr  29417  nb3grpr2  29418  nb3gr2nb  29419  cplgr3v  29470  frgr3v  30307  dipassr  30878  bnj170  34674  bnj290  34686  bnj545  34871  bnj571  34882  bnj594  34888  brapply  35902  brrestrict  35913  dfrdg4  35915  cgrid2  35967  cgr3permute3  36011  cgr3permute2  36013  cgr3permute4  36014  cgr3permute5  36015  colinearperm1  36026  colinearperm3  36027  colinearperm2  36028  colinearperm4  36029  colinearperm5  36030  colinearxfr  36039  endofsegid  36049  colinbtwnle  36082  broutsideof2  36086  dmncan2  38037  isltrn2N  40077  oeord2com  43273  uunTT1p2  44766  uunT11p1  44768  uunT12p2  44772  uunT12p4  44774  3anidm12p2  44778  uun2221p1  44785  en3lplem2VD  44815  grtriproplem  47790  grtrif1o  47793  lincvalpr  48147  alimp-no-surprise  48875