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

Theorem 3coml 1160
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 1159 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1158 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 936
This theorem is referenced by:  3comr  1161  omwordri  6774  oeword  6792  f1oen2g  7083  f1dom2g  7084  ordiso  7441  en3lplem2  7627  axdc3lem4  8289  ltasr  8931  adddir  9039  axltadd  9105  pnpcan2  9297  subdir  9424  ltaddsub  9458  leaddsub  9460  div13  9655  ltdiv2  9851  lediv2  9856  zdiv  10296  xadddir  10831  xadddi2r  10833  fzen  11028  fzrevral2  11087  fzshftral  11089  fzind2  11153  digit1  11468  faclbnd5  11544  ccatlcan  11733  elicc4abs  12078  dvdsnegb  12822  muldvds1  12829  muldvds2  12830  dvdscmul  12831  dvdsmulc  12832  dvdscmulr  12833  dvdsmulcr  12834  dvdsgcd  12998  mulgcdr  13003  coprmdvds  13057  mulgnnass  14873  gaass  15029  elfm3  17935  mettri  18335  cnmet  18759  addcnlem  18847  bcthlem5  19234  isppw2  20851  vmappw  20852  bcmono  21014  vcdir  21985  vcass  21986  imsmetlem  22135  hvaddcan2  22526  hvsubcan2  22530  mulcan2g  25143  colinearalg  25753  ax5seglem1  25771  ax5seglem2  25772  ltflcei  26140  lxflflp1  26142  fzmul  26334  rabrenfdioph  26765  uun123p2  28631  pclfinclN  30432
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