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  6586  oeword  6604  f1oen2g  6894  f1dom2g  6895  ordiso  7247  en3lplem2  7433  axdc3lem4  8095  ltasr  8738  adddir  8846  axltadd  8912  pnpcan2  9103  subdir  9230  ltaddsub  9264  leaddsub  9266  div13  9461  ltdiv2  9657  lediv2  9662  zdiv  10098  xadddir  10632  xadddi2r  10634  fzen  10827  fzrevral2  10883  fzshftral  10885  fzind2  10939  digit1  11251  faclbnd5  11327  ccatlcan  11480  elicc4abs  11819  dvdsnegb  12562  muldvds1  12569  muldvds2  12570  dvdscmul  12571  dvdsmulc  12572  dvdscmulr  12573  dvdsmulcr  12574  dvdsgcd  12738  mulgcdr  12743  coprmdvds  12797  mulgnnass  14611  gaass  14767  elfm3  17661  mettri  17932  cnmet  18297  addcnlem  18384  bcthlem5  18766  isppw2  20369  vmappw  20370  bcmono  20532  vcdir  21125  vcass  21126  imsmetlem  21275  hvaddcan2  21666  hvsubcan2  21670  mulcan2g  24100  colinearalg  24610  ax5seglem1  24628  ax5seglem2  24629  ltflcei  24998  lxflflp1  25000  cnvtr  25719  fzmul  26546  rabrenfdioph  27000  stoweidlem17  27869  uun123p2  28899  pclfinclN  30761
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