Theorem 3anrot 1093

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 1091	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1092	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 276	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 207   ∧ w3a 1080

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 208  df-an 397  df-3an 1082

This theorem is referenced by:  3anrev  1094  wefrc  5437  ordelord  6088  f13dfv  6896  fr3nr  7350  omword  8046  nnmcan  8110  modmulconst  15474  ncoprmlnprm  15897  pmtr3ncomlem1  18332  srgrmhm  18976  isphld  20480  ordtbaslem  21480  xmetpsmet  22641  comet  22806  cphassr  23499  srabn  23646  lgsdi  25592  colopp  26237  colinearalglem2  26376  umgr2edg1  26676  nb3grpr  26847  nb3grpr2  26848  nb3gr2nb  26849  cplgr3v  26900  frgr3v  27746  dipassr  28314  bnj170  31585  bnj290  31597  bnj545  31783  bnj571  31794  bnj594  31800  brapply  33008  brrestrict  33019  dfrdg4  33021  cgrid2  33073  cgr3permute3  33117  cgr3permute2  33119  cgr3permute4  33120  cgr3permute5  33121  colinearperm1  33132  colinearperm3  33133  colinearperm2  33134  colinearperm4  33135  colinearperm5  33136  colinearxfr  33145  endofsegid  33155  colinbtwnle  33188  broutsideof2  33192  dmncan2  34887  isltrn2N  36787  uunTT1p2  40668  uunT11p1  40670  uunT12p2  40674  uunT12p4  40676  3anidm12p2  40680  uun2221p1  40687  en3lplem2VD  40717  lincvalpr  43953  alimp-no-surprise  44362