Theorem 3anrot 1036

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 1035	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		df-3an 1033	. 2 ⊢ ((𝜓 ∧ 𝜒 ∧ 𝜑) ↔ ((𝜓 ∧ 𝜒) ∧ 𝜑))
4	1, 2, 3	3bitr4i 291	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 195   ∧ wa 383   ∧ w3a 1031

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

This theorem is referenced by:  3ancomb  1040  3anrev  1042  3simpc  1053  wefrc  5032  ordelord  5662  f13dfv  6430  fr3nr  6871  omword  7537  nnmcan  7601  modmulconst  14851  ncoprmlnprm  15274  pmtr3ncomlem1  17716  srgrmhm  18359  isphld  19818  ordtbaslem  20802  xmetpsmet  21963  comet  22128  cphassr  22820  srabn  22964  lgsdi  24859  colopp  25461  colinearalglem2  25587  nb3grapr  25982  nb3grapr2  25983  nb3gra2nb  25984  cusgra3v  25993  frgra3v  26529  dipassr  27085  bnj170  30017  bnj290  30029  bnj545  30219  bnj571  30230  bnj594  30236  brapply  31215  brrestrict  31226  dfrdg4  31228  cgrid2  31280  cgr3permute3  31324  cgr3permute2  31326  cgr3permute4  31327  cgr3permute5  31328  colinearperm1  31339  colinearperm3  31340  colinearperm2  31341  colinearperm4  31342  colinearperm5  31343  colinearxfr  31352  endofsegid  31362  colinbtwnle  31395  broutsideof2  31399  dmncan2  33046  isltrn2N  34424  ntrneikb  37412  ntrneixb  37413  uunTT1p2  38043  uunT11p1  38045  uunT12p2  38049  uunT12p4  38051  3anidm12p2  38055  uun2221p1  38062  en3lplem2VD  38101  umgr2edg1  40438  nb3grpr  40610  nb3grpr2  40611  nb3gr2nb  40612  cplgr3v  40657  frgr3v  41445  lincvalpr  42001  alimp-no-surprise  42336