Theorem 3anrot 1098

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 1096	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜑 ∧ 𝜒))
2		3ancomb 1097	. 2 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))
3	1, 2	bitri 274	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜓 ∧ 𝜒 ∧ 𝜑))

Syntax hints:   ↔ wb 205   ∧ w3a 1085

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 206  df-an 395  df-3an 1087

This theorem is referenced by:  3anrev  1099  wefrc  5671  ordelord  6387  f13dfv  7276  fr3nr  7763  omword  8574  nnmcan  8638  modmulconst  16237  ncoprmlnprm  16670  issubmndb  18724  pmtr3ncomlem1  19384  srgrmhm  20118  isphld  21428  ordtbaslem  22914  xmetpsmet  24076  comet  24244  cphassr  24962  srabn  25110  lgsdi  27071  divsclw  27879  colopp  28285  colinearalglem2  28430  umgr2edg1  28733  nb3grpr  28904  nb3grpr2  28905  nb3gr2nb  28906  cplgr3v  28957  frgr3v  29793  dipassr  30364  bnj170  34005  bnj290  34017  bnj545  34202  bnj571  34213  bnj594  34219  brapply  35212  brrestrict  35223  dfrdg4  35225  cgrid2  35277  cgr3permute3  35321  cgr3permute2  35323  cgr3permute4  35324  cgr3permute5  35325  colinearperm1  35336  colinearperm3  35337  colinearperm2  35338  colinearperm4  35339  colinearperm5  35340  colinearxfr  35349  endofsegid  35359  colinbtwnle  35392  broutsideof2  35396  dmncan2  37250  isltrn2N  39296  oeord2com  42365  uunTT1p2  43860  uunT11p1  43862  uunT12p2  43866  uunT12p4  43868  3anidm12p2  43872  uun2221p1  43879  en3lplem2VD  43909  lincvalpr  47188  alimp-no-surprise  47917