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

Theorem 3comr 1161
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 1160 . 2  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
323coml 1160 1  |-  ( ( ch  /\  ph  /\  ps )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  oacan  6791  omlimcl  6821  nnacan  6871  en3lplem2  7671  le2tri3i  9203  div12  9700  lemul12b  9867  zdivadd  10341  zdivmul  10342  elfz  11049  fzrev  11108  modmulnn  11265  digit2  11512  digit1  11513  faclbnd5  11589  absdiflt  12121  absdifle  12122  dvds0lem  12860  dvdsmulc  12877  dvds2add  12881  dvds2sub  12882  dvdstr  12883  pospropd  14561  fmfil  17976  elfm  17979  xmettri2  18370  stdbdmetval  18544  nmf2  18640  isvci  22061  nvtri  22159  nmooge0  22268  his7  22592  his2sub2  22595  braadd  23448  bramul  23449  cnlnadjlem2  23571  pjimai  23679  atcvati  23889  mdsymlem5  23910  brbtwn  25838  colinearalglem3  25847  colinearalg  25849  colineardim1  25995  ftc1anclem6  26285  stoweidlem2  27727  sigarperm  27826  leaddsuble  28091  fzmmmeqm  28115  swrdccatin2  28210  2cshw2lem2  28253  uun123p3  28923  bnj240  29063  bnj1189  29378
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator