MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3comr Unicode version

Theorem 3comr 1159
Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3comr  |-  ( ( ch  /\  ph  /\  ps )  ->  th )

Proof of Theorem 3comr
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213coml 1158 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1158 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  oacan  6546  omlimcl  6576  nnacan  6626  en3lplem2  7417  le2tri3i  8949  div12  9446  lemul12b  9613  zdivadd  10083  zdivmul  10084  elfz  10788  fzrev  10846  modmulnn  10988  digit2  11234  digit1  11235  faclbnd5  11311  absdiflt  11801  absdifle  11802  dvds0lem  12539  dvdsmulc  12556  dvds2add  12560  dvds2sub  12561  dvdstr  12562  pospropd  14238  fmfil  17639  elfm  17642  xmettri2  17905  stdbdmetval  18060  nmf2  18115  isvci  21138  nvtri  21236  nmooge0  21345  his7  21669  his2sub2  21672  braadd  22525  bramul  22526  cnlnadjlem2  22648  pjimai  22756  atcvati  22966  mdsymlem5  22987  brbtwn  24527  colinearalglem3  24536  colinearalg  24538  colineardim1  24684  sigarperm  27850  uun123p3  28586  bnj240  28724  bnj1189  29039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator