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

Theorem 3coml 1198
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 1197 . 2  |-  ( (
ph  /\  ch  /\  ps )  ->  th )
323com13 1196 1  |-  ( ( ps  /\  ch  /\  ph )  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 968
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 970
This theorem is referenced by:  3comr  1199  omwordri  7213  oeword  7231  f1oen2g  7524  f1dom2g  7525  ordiso  7932  en3lplem2  8023  axdc3lem4  8824  ltasr  9468  adddir  9578  axltadd  9649  pnpcan2  9850  subdir  9982  ltaddsub  10017  leaddsub  10019  mulcan2g  10194  div13  10219  ltdiv2  10421  lediv2  10426  zdiv  10922  xadddir  11479  xadddi2r  11481  fzen  11694  fzrevral2  11754  fzshftral  11756  ssfzoulel  11865  fzind2  11883  digit1  12257  faclbnd5  12333  ccatlcan  12649  elicc4abs  13103  dvdsnegb  13853  muldvds1  13860  muldvds2  13861  dvdscmul  13862  dvdsmulc  13863  dvdscmulr  13864  dvdsmulcr  13865  dvdsgcd  14031  mulgcdr  14036  coprmdvds  14093  mulgnnass  15965  gaass  16125  elfm3  20181  mettri  20585  cnmet  21009  addcnlem  21098  bcthlem5  21497  isppw2  23112  vmappw  23113  bcmono  23275  colinearalg  23884  ax5seglem1  23902  ax5seglem2  23903  vcdir  25110  vcass  25111  imsmetlem  25260  hvaddcan2  25652  hvsubcan2  25656  ltflcei  29608  lxflflp1  29610  fzmul  29825  rabrenfdioph  30341  uun123p2  32564  isosctrlem1ALT  32691  pclfinclN  34623
  Copyright terms: Public domain W3C validator