Theorem 3anrot 1060

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 465	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
2		3anass 1059	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		df-3an 1056	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
4	1, 2, 3	3bitr4i 292	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 196   ∧ wa 383   ∧ w3a 1054

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 385  df-3an 1056

This theorem is referenced by:  3ancomb  1064  3anrev  1067  3simpc  1080  wefrc  5137  ordelord  5783  f13dfv  6570  fr3nr  7021  omword  7695  nnmcan  7759  modmulconst  15060  ncoprmlnprm  15483  pmtr3ncomlem1  17939  srgrmhm  18582  isphld  20047  ordtbaslem  21040  xmetpsmet  22200  comet  22365  cphassr  23058  srabn  23202  lgsdi  25104  colopp  25706  colinearalglem2  25832  umgr2edg1  26148  nb3grpr  26328  nb3grpr2  26329  nb3gr2nb  26330  cplgr3v  26387  frgr3v  27255  dipassr  27829  bnj170  30892  bnj290  30904  bnj545  31091  bnj571  31102  bnj594  31108  brapply  32170  brrestrict  32181  dfrdg4  32183  cgrid2  32235  cgr3permute3  32279  cgr3permute2  32281  cgr3permute4  32282  cgr3permute5  32283  colinearperm1  32294  colinearperm3  32295  colinearperm2  32296  colinearperm4  32297  colinearperm5  32298  colinearxfr  32307  endofsegid  32317  colinbtwnle  32350  broutsideof2  32354  dmncan2  34006  isltrn2N  35724  ntrneikb  38709  ntrneixb  38710  uunTT1p2  39339  uunT11p1  39341  uunT12p2  39345  uunT12p4  39347  3anidm12p2  39351  uun2221p1  39358  en3lplem2VD  39393  lincvalpr  42532  alimp-no-surprise  42855