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

Theorem simpr1 1000
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )

Proof of Theorem simpr1
StepHypRef Expression
1 simp1 994 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 464 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971
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 369  df-3an 973
This theorem is referenced by:  simplr1  1036  simprr1  1042  simp1r1  1090  simp2r1  1096  simp3r1  1102  3anandis  1328  isopolem  6216  fr3nr  6588  suppfnss  6917  frfi  7757  intrnfi  7868  iinfi  7869  eqsup  7907  fisupcl  7919  cnfcomlem  8134  cnfcomlemOLD  8142  ackbij1lem15  8605  fpwwe2lem5  9001  dedekindle  9734  ico0  11578  elioc2  11590  elico2  11591  elicc2  11592  iccsplit  11656  fseq1p1m1  11756  elfz0ubfz0  11782  hashtpg  12507  swrdsbslen  12664  swrdspsleq  12665  ccatswrd  12672  tanadd  13984  dvds2ln  14098  qredeq  14331  ressress  14781  mreexexlem4d  15136  mreexexd  15137  0catg  15176  2oppccomf  15213  issubc3  15337  fthmon  15415  fuccocl  15452  fucidcl  15453  invfuc  15462  initoeu2lem0  15491  initoeu2lem1  15492  curf2cl  15699  yonedalem4c  15745  yonedalem3  15748  pospo  15802  latjle12  15891  latjlej1  15894  latnlej2  15900  latlem12  15907  latmlem1  15910  latledi  15918  latmlej11  15919  latjass  15924  latj12  15925  latj32  15926  latj13  15927  latj31  15928  latjrot  15929  latjjdi  15932  latjjdir  15933  latdisdlem  16018  prdsmndd  16152  imasmnd2  16156  frmdmnd  16226  grpsubrcan  16318  grpsubadd  16325  grpsubsub  16326  grpaddsubass  16327  grpsubsub4  16330  grpnnncan2  16334  mulgnndir  16363  mulgnn0dir  16364  mulgdir  16366  mulgnnass  16369  mulgnn0ass  16370  mulgass  16371  mulgsubdir  16372  pwsmulg  16383  imasgrp2  16384  issubg2  16415  eqgval  16449  qusgrp  16455  galcan  16541  gacan  16542  oppgmnd  16588  symggrp  16624  pmtrprfv  16677  pmtr3ncom  16699  psgnunilem3  16720  cmn32  17015  cmn12  17017  abladdsub  17024  mulgnn0di  17033  mulgdi  17034  mulgsubdi  17037  dprdss  17271  dprdz  17272  dprdf1o  17274  dprdsn  17278  dprd2da  17286  ablfac1b  17316  pgpfac1lem5  17325  srgbinomlem2  17387  srgbinom  17391  ringi  17406  prdsringd  17456  imasring  17463  opprring  17475  mulgass3  17481  dvrass  17534  kerf1hrm  17587  subrgunit  17642  issubrg2  17644  abvdiv  17681  islss3  17800  prdslmodd  17810  islmhm2  17879  lspsolv  17984  islbs2  17995  islbs3  17996  lbsextlem4  18002  sralmod  18028  issubassa  18168  sraassa  18169  psrbaglecl  18214  psrbagcon  18217  psrgrp  18246  psrlmod  18249  psrring  18261  psrassa  18264  ipdir  18847  ipdi  18848  ipsubdir  18850  ipsubdi  18851  ipass  18853  ipassr  18854  ipassr2  18855  ocvlss  18876  mamudm  19057  matring  19112  matassa  19113  ofco2  19120  mdetunilem1  19281  mdetunilem9  19289  mdetuni0  19290  mdetmul  19292  gsummatr01lem3  19326  iinopn  19578  subbascn  19922  nrmsep2  20024  isnrm3  20027  regsep2  20044  dnsconst  20046  dfcon2  20086  1stcelcls  20128  nllyidm  20156  dislly  20164  upxp  20290  fbasne0  20497  filss  20520  infil  20530  fsubbas  20534  filssufilg  20578  tmdcn2  20754  psmettri  20981  isxmet2d  20996  xmettri  21020  xmetres2  21030  bldisj  21067  blss2ps  21072  blss2  21073  xmstri2  21135  mstri2  21136  xmstri  21137  mstri  21138  xmstri3  21139  mstri3  21140  msrtri  21141  comet  21182  stdbdbl  21186  met2ndci  21191  ngprcan  21295  ngplcan  21296  ngpsubcan  21299  nrgdsdi  21340  nrgdsdir  21341  nlmdsdi  21356  nlmdsdir  21357  blcvx  21469  icccmplem2  21494  pi1grplem  21715  pi1cof  21725  cvsdiv  21775  cvsdivcl  21776  cphdivcl  21795  cphsubdir  21820  cphsubdi  21821  cphassr  21824  bcthlem5  21933  rrxcph  21990  volfiniun  22123  volcn  22181  itg1val2  22257  dvconst  22486  dvlip  22560  dvfsumlem4  22596  ftc1a  22604  ulmval  22941  ulmdvlem3  22963  ang180  23345  cvxcl  23512  scvxcvx  23513  sgmmul  23674  logexprlim  23698  dchrabl  23727  motgrp  24131  f1otrge  24377  colinearalglem1  24411  colinearalg  24415  axcgrtr  24420  axlowdimlem16  24462  axeuclidlem  24467  axcontlem7  24475  eengtrkg  24490  eengtrkge  24491  wlkoniswlk  24738  constr2trl  24803  wlkdvspth  24812  erclwwlktr  25017  erclwwlkntr  25029  el2spthonot0  25073  el2wlkonotot0  25074  usg2wotspth  25086  2pthwlkonot  25087  iseupa  25167  numclwwlk5  25314  friendship  25324  grpodivdiv  25448  grpomuldivass  25449  grpopnpcan2  25453  ablodivdiv4  25491  ablonnncan  25493  ablonnncan1  25495  zerdivemp1  25634  nvmdi  25743  dipassr  25959  archiabllem2c  27973  dvrdir  28015  dvrcan5  28018  reofld  28065  pstmfval  28110  tpr2rico  28129  qqhval2lem  28196  qqhvq  28202  issiga  28341  measdivcstOLD  28432  measdivcst  28433  carsggect  28526  signsply0  28772  erdszelem9  28907  rescon  28955  cvmseu  28985  cvmlift2lem12  29023  elmrsubrn  29144  mclsind  29194  cgrid2  29881  segconeu  29889  btwncomim  29891  btwnswapid  29895  cgrxfr  29933  btwnxfr  29934  colineardim1  29939  brofs2  29955  brifs2  29956  idinside  29962  endofsegid  29963  btwnconn1lem7  29971  btwnconn1lem11  29975  btwnconn1  29979  segcon2  29983  seglemin  29991  segletr  29992  btwnsegle  29995  colinbtwnle  29996  broutsideof2  30000  broutsideof3  30004  outsidele  30010  fvray  30019  fvline  30022  linerflx1  30027  ellines  30030  ftc1anc  30338  ivthALT  30393  sdclem1  30476  sstotbnd2  30510  zerdivemp1x  30598  isdrngo2  30601  iscringd  30636  irrapxlem6  31002  jm2.26lem3  31182  dgrsub2  31325  mpaadgr  31344  mendring  31382  mendlmod  31383  mendassa  31384  fmuldfeq  31816  stoweidlem43  32064  stoweidlem52  32073  stoweidlem53  32074  stoweidlem56  32077  stoweidlem57  32078  usgfis  32818  usgfisALT  32822  copissgrp  32868  cznrng  33017  funcringcsetcALTV2lem9  33106  funcringcsetclem9ALTV  33129  ply1ass23l  33236  linccl  33269  lincext1  33309  lincext3  33311  lincresunit2  33333  bnj149  34334  bnj1118  34441  bnj1128  34447  lsmsat  35130  lfladdcl  35193  lflnegcl  35197  lflvscl  35199  lshpkrlem4  35235  lshpkrlem6  35237  ldualgrplem  35267  lduallmodlem  35274  latmassOLD  35351  latm12  35352  latm32  35353  latmrot  35354  latmmdiN  35356  latmmdir  35357  omlfh1N  35380  omlfh3N  35381  cvlexchb1  35452  cvlexch3  35454  cvlexch4N  35455  cvlatexchb1  35456  cvlsupr2  35465  hlatjass  35491  hlatj12  35492  hlatj32  35493  cvratlem  35542  cvrat  35543  atcvrj0  35549  cvrat2  35550  atltcvr  35556  atexchltN  35562  cvrat3  35563  cvrat4  35564  3dimlem3  35582  3dimlem3OLDN  35583  3at  35611  2atneat  35636  llncmp  35643  2at0mat0  35646  2atmat0  35647  lplnnle2at  35662  llncvrlpln  35679  lplncmp  35683  lplnexllnN  35685  2llnjaN  35687  4atlem11  35730  lplncvrlvol  35737  lvolcmp  35738  2atm2atN  35906  elpaddatriN  35924  paddasslem9  35949  paddass  35959  padd12N  35960  paddssw2  35965  paddss  35966  pmodlem2  35968  pmodN  35971  pmapjlln1  35976  atmod1i1  35978  atmod1i2  35980  pexmidlem2N  36092  pexmidlem6N  36096  pl42N  36104  lhpm0atN  36150  lautlt  36212  lautcvr  36213  lautj  36214  lautm  36215  ltrneq2  36269  cdlemc3  36315  cdlemc4  36316  cdlemd1  36320  cdleme1b  36348  cdleme1  36349  cdleme2  36350  cdleme3e  36354  cdlemefr27cl  36526  cdlemefs27cl  36536  cdleme42mN  36610  cdlemftr2  36689  trljco  36863  tgrpgrplem  36872  tendoplass  36906  tendodi1  36907  tendodi2  36908  cdlemk36  37036  erngdvlem3  37113  erngdvlem3-rN  37121  tendospdi1  37144  dvalveclem  37149  dialss  37170  dvhvaddass  37221  dvhopvsca  37226  dvhlveclem  37232  diblss  37294  diclss  37317  dihmeetlem12N  37442  dihmeetlem15N  37445  dihmeetlem16N  37446  dihmeetlem17N  37447  dihmeetlem18N  37448  dihmeetlem19N  37449  dvh4dimN  37571  lpolvN  37610  lclkr  37657  lclkrs  37663  lcfr  37709  iunrelexpmin2  38208  relexpxpmin  38226  relexpmulg  38228
  Copyright terms: Public domain W3C validator