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

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

Proof of Theorem 3coml
StepHypRef Expression
1 3exp.1 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213com23 1203 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1202 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  3comr  1205  omwordri  7257  oeword  7275  f1oen2g  7569  f1dom2g  7570  ordiso  7974  en3lplem2  8064  axdc3lem4  8864  ltasr  9506  adddir  9616  axltadd  9688  pnpcan2  9894  subdir  10031  ltaddsub  10066  leaddsub  10068  mulcan2g  10243  div13  10268  ltdiv2  10469  lediv2  10474  zdiv  10973  xadddir  11540  xadddi2r  11542  fzen  11755  fzrevral2  11817  fzshftral  11819  ssfzoulel  11941  fzind2  11959  flflp1  11979  digit1  12342  faclbnd5  12418  ccatlcan  12751  relexpreld  13020  elicc4abs  13299  dvdsnegb  14208  muldvds1  14215  muldvds2  14216  dvdscmul  14217  dvdsmulc  14218  dvdscmulr  14219  dvdsmulcr  14220  dvdsgcd  14388  mulgcdr  14393  coprmdvds  14450  mulgnnass  16492  gaass  16657  elfm3  20741  mettri  21145  cnmet  21569  addcnlem  21658  bcthlem5  22057  isppw2  23768  vmappw  23769  bcmono  23931  colinearalg  24617  ax5seglem1  24635  ax5seglem2  24636  vcdir  25846  vcass  25847  imsmetlem  25996  hvaddcan2  26388  hvsubcan2  26392  isbasisrelowllem1  31259  ltflcei  31395  fzmul  31495  pclfinclN  32947  rabrenfdioph  35089  lcmgcdeq  36044  uun123p2  36611  isosctrlem1ALT  36745
  Copyright terms: Public domain W3C validator