MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3coml Structured version   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  6815  oeword  6833  f1oen2g  7124  f1dom2g  7125  ordiso  7485  en3lplem2  7671  axdc3lem4  8333  ltasr  8975  adddir  9083  axltadd  9149  pnpcan2  9341  subdir  9468  ltaddsub  9502  leaddsub  9504  div13  9699  ltdiv2  9895  lediv2  9900  zdiv  10340  xadddir  10875  xadddi2r  10877  fzen  11072  fzrevral2  11132  fzshftral  11134  fzind2  11198  digit1  11513  faclbnd5  11589  ccatlcan  11778  elicc4abs  12123  dvdsnegb  12867  muldvds1  12874  muldvds2  12875  dvdscmul  12876  dvdsmulc  12877  dvdscmulr  12878  dvdsmulcr  12879  dvdsgcd  13043  mulgcdr  13048  coprmdvds  13102  mulgnnass  14918  gaass  15074  elfm3  17982  mettri  18382  cnmet  18806  addcnlem  18894  bcthlem5  19281  isppw2  20898  vmappw  20899  bcmono  21061  vcdir  22032  vcass  22033  imsmetlem  22182  hvaddcan2  22573  hvsubcan2  22577  mulcan2g  25190  colinearalg  25849  ax5seglem1  25867  ax5seglem2  25868  ltflcei  26239  lxflflp1  26241  fzmul  26444  rabrenfdioph  26875  swrdvalodmlem1  28187  2cshw2lem2  28253  2cshw2lem3  28254  uun123p2  28922  isosctrlem1ALT  29046  pclfinclN  30747
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