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

Theorem 3coml 1194
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 1193 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1192 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  3comr  1195  omwordri  7010  oeword  7028  f1oen2g  7325  f1dom2g  7326  ordiso  7729  en3lplem2  7820  axdc3lem4  8621  ltasr  9266  adddir  9376  axltadd  9447  pnpcan2  9648  subdir  9778  ltaddsub  9812  leaddsub  9814  mulcan2g  9989  div13  10014  ltdiv2  10216  lediv2  10221  zdiv  10711  xadddir  11258  xadddi2r  11260  fzen  11466  fzrevral2  11544  fzshftral  11546  ssfzoulel  11620  fzind2  11636  digit1  11997  faclbnd5  12073  ccatlcan  12365  elicc4abs  12806  dvdsnegb  13549  muldvds1  13556  muldvds2  13557  dvdscmul  13558  dvdsmulc  13559  dvdscmulr  13560  dvdsmulcr  13561  dvdsgcd  13726  mulgcdr  13731  coprmdvds  13787  mulgnnass  15654  gaass  15814  elfm3  19522  mettri  19926  cnmet  20350  addcnlem  20439  bcthlem5  20838  isppw2  22452  vmappw  22453  bcmono  22615  colinearalg  23155  ax5seglem1  23173  ax5seglem2  23174  vcdir  23930  vcass  23931  imsmetlem  24080  hvaddcan2  24472  hvsubcan2  24476  ltflcei  28417  lxflflp1  28419  fzmul  28634  rabrenfdioph  29151  uun123p2  31541  isosctrlem1ALT  31668  pclfinclN  33592
  Copyright terms: Public domain W3C validator