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

Theorem 3comr 1204
Description: Commutation in antecedent. Rotate right. (Contributed by NM, 28-Jan-1996.)
Hypothesis
Ref Expression
3exp.1
Assertion
Ref Expression
3comr

Proof of Theorem 3comr
StepHypRef Expression
1 3exp.1 . . 3
213coml 1203 . 2
323coml 1203 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  oacan  7216  omlimcl  7246  nnacan  7296  en3lplem2  8053  le2tri3i  9735  ltaddsublt  10201  div12  10254  lemul12b  10424  zdivadd  10959  zdivmul  10960  elfz  11707  fzmmmeqm  11746  fzrev  11771  modmulnn  12013  digit2  12299  digit1  12300  faclbnd5  12376  swrdccatin2  12712  absdiflt  13150  absdifle  13151  dvds0lem  13994  dvdsmulc  14011  dvds2add  14015  dvds2sub  14016  dvdstr  14018  mulmoddvds  14044  pospropd  15764  fmfil  20445  elfm  20448  psmettri2  20813  xmettri2  20843  stdbdmetval  21017  nmf2  21113  brbtwn  24202  colinearalglem3  24211  colinearalg  24213  isvci  25475  nvtri  25573  nmooge0  25682  his7  26007  his2sub2  26010  braadd  26864  bramul  26865  cnlnadjlem2  26987  pjimai  27095  atcvati  27305  mdsymlem5  27326  colineardim1  29711  ftc1anclem6  30095  lcmdvds  31214  stoweidlem2  31784  sigarperm  32077  leaddsuble  32319  uun123p3  33608  bnj240  33751  bnj1189  34065
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator