Theorem 3anrot 1043

Description: Rotation law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3anrot	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Proof of Theorem 3anrot

Step	Hyp	Ref	Expression
1		ancom 466	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
2		3anass 1042	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		df-3an 1039	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
4	1, 2, 3	3bitr4i 292	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 196   ∧ wa 384   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  3ancomb  1047  3anrev  1049  3simpc  1060  wefrc  5108  ordelord  5745  f13dfv  6530  fr3nr  6979  omword  7650  nnmcan  7714  modmulconst  15013  ncoprmlnprm  15436  pmtr3ncomlem1  17893  srgrmhm  18536  isphld  19999  ordtbaslem  20992  xmetpsmet  22153  comet  22318  cphassr  23012  srabn  23156  lgsdi  25059  colopp  25661  colinearalglem2  25787  umgr2edg1  26103  nb3grpr  26284  nb3grpr2  26285  nb3gr2nb  26286  cplgr3v  26331  frgr3v  27139  dipassr  27701  bnj170  30764  bnj290  30776  bnj545  30965  bnj571  30976  bnj594  30982  brapply  32045  brrestrict  32056  dfrdg4  32058  cgrid2  32110  cgr3permute3  32154  cgr3permute2  32156  cgr3permute4  32157  cgr3permute5  32158  colinearperm1  32169  colinearperm3  32170  colinearperm2  32171  colinearperm4  32172  colinearperm5  32173  colinearxfr  32182  endofsegid  32192  colinbtwnle  32225  broutsideof2  32229  dmncan2  33876  isltrn2N  35406  ntrneikb  38392  ntrneixb  38393  uunTT1p2  39022  uunT11p1  39024  uunT12p2  39028  uunT12p4  39030  3anidm12p2  39034  uun2221p1  39041  en3lplem2VD  39079  lincvalpr  42207  alimp-no-surprise  42527