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

This theorem is referenced by:  3anrev  1099  wefrc  5666  ordelord  6385  f13dfv  7277  fr3nr  7768  omword  8584  nnmcan  8648  modmulconst  16258  ncoprmlnprm  16693  issubmndb  18750  pmtr3ncomlem1  19421  srgrmhm  20155  isphld  21579  ordtbaslem  23085  xmetpsmet  24247  comet  24415  cphassr  25133  srabn  25281  lgsdi  27260  divsclw  28087  colopp  28566  colinearalglem2  28711  umgr2edg1  29017  nb3grpr  29188  nb3grpr2  29189  nb3gr2nb  29190  cplgr3v  29241  frgr3v  30078  dipassr  30649  bnj170  34323  bnj290  34335  bnj545  34520  bnj571  34531  bnj594  34537  brapply  35528  brrestrict  35539  dfrdg4  35541  cgrid2  35593  cgr3permute3  35637  cgr3permute2  35639  cgr3permute4  35640  cgr3permute5  35641  colinearperm1  35652  colinearperm3  35653  colinearperm2  35654  colinearperm4  35655  colinearperm5  35656  colinearxfr  35665  endofsegid  35675  colinbtwnle  35708  broutsideof2  35712  dmncan2  37544  isltrn2N  39587  oeord2com  42734  uunTT1p2  44228  uunT11p1  44230  uunT12p2  44234  uunT12p4  44236  3anidm12p2  44240  uun2221p1  44247  en3lplem2VD  44277  lincvalpr  47480  alimp-no-surprise  48208

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »