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  5619  ordelord  6340  f13dfv  7223  fr3nr  7720  omword  8499  nnmcan  8564  modmulconst  16251  ncoprmlnprm  16692  issubmndb  18767  pmtr3ncomlem1  19442  srgrmhm  20197  isphld  21647  ordtbaslem  23166  xmetpsmet  24326  comet  24491  cphassr  25192  srabn  25340  lgsdi  27314  divsclw  28204  colopp  28854  colinearalglem2  28993  umgr2edg1  29297  nb3grpr  29468  nb3grpr2  29469  nb3gr2nb  29470  cplgr3v  29521  frgr3v  30363  dipassr  30935  bnj170  34860  bnj290  34872  bnj545  35056  bnj571  35067  bnj594  35073  brapply  36137  brrestrict  36150  dfrdg4  36152  cgrid2  36204  cgr3permute3  36248  cgr3permute2  36250  cgr3permute4  36251  cgr3permute5  36252  colinearperm1  36263  colinearperm3  36264  colinearperm2  36265  colinearperm4  36266  colinearperm5  36267  colinearxfr  36276  endofsegid  36286  colinbtwnle  36319  broutsideof2  36323  dmncan2  38415  isltrn2N  40583  oeord2com  43760  uunTT1p2  45242  uunT11p1  45244  uunT12p2  45248  uunT12p4  45250  3anidm12p2  45254  uun2221p1  45261  en3lplem2VD  45291  grtriproplem  48430  grtrif1o  48433  lincvalpr  48909  alimp-no-surprise  50271