Theorem 3anrot 1097

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

Syntax hints:   ↔ wb 205   ∧ w3a 1084

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

This theorem is referenced by:  3anrev  1098  wefrc  5663  ordelord  6380  f13dfv  7268  fr3nr  7756  omword  8571  nnmcan  8635  modmulconst  16238  ncoprmlnprm  16673  issubmndb  18730  pmtr3ncomlem1  19393  srgrmhm  20127  isphld  21547  ordtbaslem  23047  xmetpsmet  24209  comet  24377  cphassr  25095  srabn  25243  lgsdi  27222  divsclw  28049  colopp  28528  colinearalglem2  28673  umgr2edg1  28976  nb3grpr  29147  nb3grpr2  29148  nb3gr2nb  29149  cplgr3v  29200  frgr3v  30037  dipassr  30608  bnj170  34238  bnj290  34250  bnj545  34435  bnj571  34446  bnj594  34452  brapply  35443  brrestrict  35454  dfrdg4  35456  cgrid2  35508  cgr3permute3  35552  cgr3permute2  35554  cgr3permute4  35555  cgr3permute5  35556  colinearperm1  35567  colinearperm3  35568  colinearperm2  35569  colinearperm4  35570  colinearperm5  35571  colinearxfr  35580  endofsegid  35590  colinbtwnle  35623  broutsideof2  35627  dmncan2  37458  isltrn2N  39504  oeord2com  42642  uunTT1p2  44137  uunT11p1  44139  uunT12p2  44143  uunT12p4  44145  3anidm12p2  44149  uun2221p1  44156  en3lplem2VD  44186  lincvalpr  47379  alimp-no-surprise  48107