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

Theorem 3coml 1158
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 1157 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1156 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  3comr  1159  omwordri  6570  oeword  6588  f1oen2g  6878  f1dom2g  6879  ordiso  7231  en3lplem2  7417  axdc3lem4  8079  ltasr  8722  adddir  8830  axltadd  8896  pnpcan2  9087  subdir  9214  ltaddsub  9248  leaddsub  9250  div13  9445  ltdiv2  9641  lediv2  9646  zdiv  10082  xadddir  10616  xadddi2r  10618  fzen  10811  fzrevral2  10867  fzshftral  10869  fzind2  10923  digit1  11235  faclbnd5  11311  ccatlcan  11464  elicc4abs  11803  dvdsnegb  12546  muldvds1  12553  muldvds2  12554  dvdscmul  12555  dvdsmulc  12556  dvdscmulr  12557  dvdsmulcr  12558  dvdsgcd  12722  mulgcdr  12727  coprmdvds  12781  mulgnnass  14595  gaass  14751  elfm3  17645  mettri  17916  cnmet  18281  addcnlem  18368  bcthlem5  18750  isppw2  20353  vmappw  20354  bcmono  20516  vcdir  21109  vcass  21110  imsmetlem  21259  hvaddcan2  21650  hvsubcan2  21654  mulcan2g  23496  colinearalg  23949  ax5seglem1  23967  ax5seglem2  23968  cnvtr  25028  fzmul  25855  rabrenfdioph  26309  stoweidlem17  27178  uun123p2  27958  pclfinclN  29512
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