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  5022  ordelord  5648  f13dfv  6408  fr3nr  6849  omword  7515  nnmcan  7579  modmulconst  14800  ncoprmlnprm  15223  pmtr3ncomlem1  17665  srgrmhm  18308  isphld  19766  ordtbaslem  20750  xmetpsmet  21911  comet  22076  cphassr  22765  srabn  22909  lgsdi  24804  colopp  25407  colinearalglem2  25533  nb3grapr  25776  nb3grapr2  25777  nb3gra2nb  25778  cusgra3v  25787  frgra3v  26323  dipassr  26879  bnj170  29811  bnj290  29823  bnj545  30013  bnj571  30024  bnj594  30030  brapply  31009  brrestrict  31020  dfrdg4  31022  cgrid2  31074  cgr3permute3  31118  cgr3permute2  31120  cgr3permute4  31121  cgr3permute5  31122  colinearperm1  31133  colinearperm3  31134  colinearperm2  31135  colinearperm4  31136  colinearperm5  31137  colinearxfr  31146  endofsegid  31156  colinbtwnle  31189  broutsideof2  31193  dmncan2  32840  isltrn2N  34218  ntrneikb  37206  ntrneixb  37207  uunTT1p2  37837  uunT11p1  37839  uunT12p2  37843  uunT12p4  37845  3anidm12p2  37849  uun2221p1  37856  en3lplem2VD  37895  umgr2edg1  40430  nb3grpr  40602  nb3grpr2  40603  nb3gr2nb  40604  cplgr3v  40649  frgr3v  41437  lincvalpr  41993  alimp-no-surprise  42289