Theorem 3anrot 1099

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

Syntax hints:   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3anrev  1100  wefrc  5613  ordelord  6329  f13dfv  7211  fr3nr  7708  omword  8488  nnmcan  8552  modmulconst  16199  ncoprmlnprm  16639  issubmndb  18679  pmtr3ncomlem1  19352  srgrmhm  20107  isphld  21561  ordtbaslem  23073  xmetpsmet  24234  comet  24399  cphassr  25110  srabn  25258  lgsdi  27243  divsclw  28103  colopp  28714  colinearalglem2  28852  umgr2edg1  29156  nb3grpr  29327  nb3grpr2  29328  nb3gr2nb  29329  cplgr3v  29380  frgr3v  30219  dipassr  30790  bnj170  34665  bnj290  34677  bnj545  34862  bnj571  34873  bnj594  34879  brapply  35912  brrestrict  35923  dfrdg4  35925  cgrid2  35977  cgr3permute3  36021  cgr3permute2  36023  cgr3permute4  36024  cgr3permute5  36025  colinearperm1  36036  colinearperm3  36037  colinearperm2  36038  colinearperm4  36039  colinearperm5  36040  colinearxfr  36049  endofsegid  36059  colinbtwnle  36092  broutsideof2  36096  dmncan2  38057  isltrn2N  40099  oeord2com  43284  uunTT1p2  44768  uunT11p1  44770  uunT12p2  44774  uunT12p4  44776  3anidm12p2  44780  uun2221p1  44787  en3lplem2VD  44817  grtriproplem  47923  grtrif1o  47926  lincvalpr  48403  alimp-no-surprise  49766