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

Theorem 3coml 1161
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 1160 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1159 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  3comr  1162  omwordri  6818  oeword  6836  f1oen2g  7127  f1dom2g  7128  ordiso  7488  en3lplem2  7674  axdc3lem4  8338  ltasr  8980  adddir  9088  axltadd  9154  pnpcan2  9346  subdir  9473  ltaddsub  9507  leaddsub  9509  div13  9704  ltdiv2  9900  lediv2  9905  zdiv  10345  xadddir  10880  xadddi2r  10882  fzen  11077  fzrevral2  11137  fzshftral  11139  fzind2  11203  digit1  11518  faclbnd5  11594  ccatlcan  11783  elicc4abs  12128  dvdsnegb  12872  muldvds1  12879  muldvds2  12880  dvdscmul  12881  dvdsmulc  12882  dvdscmulr  12883  dvdsmulcr  12884  dvdsgcd  13048  mulgcdr  13053  coprmdvds  13107  mulgnnass  14923  gaass  15079  elfm3  17987  mettri  18387  cnmet  18811  addcnlem  18899  bcthlem5  19286  isppw2  20903  vmappw  20904  bcmono  21066  vcdir  22037  vcass  22038  imsmetlem  22187  hvaddcan2  22578  hvsubcan2  22582  mulcan2g  25195  colinearalg  25854  ax5seglem1  25872  ax5seglem2  25873  ltflcei  26247  lxflflp1  26249  fzmul  26458  rabrenfdioph  26889  swrdvalodmlem1  28221  2cshw2lem2  28287  2cshw2lem3  28288  uun123p2  28996  isosctrlem1ALT  29120  pclfinclN  30821
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator