Theorem 3anrot 1100

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

Syntax hints:   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anrev  1101  wefrc  5625  ordelord  6345  f13dfv  7229  fr3nr  7726  omword  8505  nnmcan  8570  modmulconst  16257  ncoprmlnprm  16698  issubmndb  18773  pmtr3ncomlem1  19448  srgrmhm  20203  isphld  21634  ordtbaslem  23153  xmetpsmet  24313  comet  24478  cphassr  25179  srabn  25327  lgsdi  27297  divsclw  28187  colopp  28837  colinearalglem2  28976  umgr2edg1  29280  nb3grpr  29451  nb3grpr2  29452  nb3gr2nb  29453  cplgr3v  29504  frgr3v  30345  dipassr  30917  bnj170  34841  bnj290  34853  bnj545  35037  bnj571  35048  bnj594  35054  brapply  36118  brrestrict  36131  dfrdg4  36133  cgrid2  36185  cgr3permute3  36229  cgr3permute2  36231  cgr3permute4  36232  cgr3permute5  36233  colinearperm1  36244  colinearperm3  36245  colinearperm2  36246  colinearperm4  36247  colinearperm5  36248  colinearxfr  36257  endofsegid  36267  colinbtwnle  36300  broutsideof2  36304  dmncan2  38398  isltrn2N  40566  oeord2com  43739  uunTT1p2  45221  uunT11p1  45223  uunT12p2  45227  uunT12p4  45229  3anidm12p2  45233  uun2221p1  45240  en3lplem2VD  45270  grtriproplem  48415  grtrif1o  48418  lincvalpr  48894  alimp-no-surprise  50256