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  5679  ordelord  6406  f13dfv  7294  fr3nr  7792  omword  8608  nnmcan  8672  modmulconst  16325  ncoprmlnprm  16765  issubmndb  18818  pmtr3ncomlem1  19491  srgrmhm  20219  isphld  21672  ordtbaslem  23196  xmetpsmet  24358  comet  24526  cphassr  25246  srabn  25394  lgsdi  27378  divsclw  28220  colopp  28777  colinearalglem2  28922  umgr2edg1  29228  nb3grpr  29399  nb3grpr2  29400  nb3gr2nb  29401  cplgr3v  29452  frgr3v  30294  dipassr  30865  bnj170  34712  bnj290  34724  bnj545  34909  bnj571  34920  bnj594  34926  brapply  35939  brrestrict  35950  dfrdg4  35952  cgrid2  36004  cgr3permute3  36048  cgr3permute2  36050  cgr3permute4  36051  cgr3permute5  36052  colinearperm1  36063  colinearperm3  36064  colinearperm2  36065  colinearperm4  36066  colinearperm5  36067  colinearxfr  36076  endofsegid  36086  colinbtwnle  36119  broutsideof2  36123  dmncan2  38084  isltrn2N  40122  oeord2com  43324  uunTT1p2  44815  uunT11p1  44817  uunT12p2  44821  uunT12p4  44823  3anidm12p2  44827  uun2221p1  44834  en3lplem2VD  44864  grtriproplem  47906  grtrif1o  47909  lincvalpr  48335  alimp-no-surprise  49300