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

Theorem simpr1 1014
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 1008 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ps )
21adantl 468 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  simplr1  1050  simprr1  1056  simp1r1  1104  simp2r1  1110  simp3r1  1116  3anandis  1371  fpr2g  6125  isopolem  6236  fr3nr  6606  suppfnss  6940  frfi  7816  intrnfi  7930  iinfi  7931  eqsup  7970  fisupcl  7985  cnfcomlem  8204  ackbij1lem15  8664  fpwwe2lem5  9059  dedekindle  9798  ico0  11682  elioc2  11697  elico2  11698  elicc2  11699  iccsplit  11765  fseq1p1m1  11868  elfz0ubfz0  11894  hashtpg  12641  swrdsbslen  12804  swrdspsleq  12805  ccatswrd  12812  tanadd  14221  dvds2ln  14333  qredeq  14663  ressress  15187  mreexexlem4d  15553  mreexexd  15554  0catg  15593  2oppccomf  15630  issubc3  15754  fthmon  15832  fuccocl  15869  fucidcl  15870  invfuc  15879  initoeu2lem0  15908  initoeu2lem1  15909  curf2cl  16116  yonedalem4c  16162  yonedalem3  16165  pospo  16219  latjle12  16308  latjlej1  16311  latnlej2  16317  latlem12  16324  latmlem1  16327  latledi  16335  latmlej11  16336  latjass  16341  latj12  16342  latj32  16343  latj13  16344  latj31  16345  latjrot  16346  latjjdi  16349  latjjdir  16350  latdisdlem  16435  prdsmndd  16569  imasmnd2  16573  frmdmnd  16643  grpsubrcan  16735  grpsubadd  16742  grpsubsub  16743  grpaddsubass  16744  grpsubsub4  16747  grpnnncan2  16751  mulgnndir  16780  mulgnn0dir  16781  mulgdir  16783  mulgnnass  16786  mulgnn0ass  16787  mulgass  16788  mulgsubdir  16789  pwsmulg  16800  imasgrp2  16801  issubg2  16832  eqgval  16866  qusgrp  16872  galcan  16958  gacan  16959  oppgmnd  17005  symggrp  17041  pmtrprfv  17094  pmtr3ncom  17116  psgnunilem3  17137  cmn32  17448  cmn12  17450  abladdsub  17457  mulgnn0di  17466  mulgdi  17467  mulgsubdi  17470  dprdss  17662  dprdz  17663  dprdf1o  17665  dprdsn  17669  dprd2da  17675  ablfac1b  17703  pgpfac1lem5  17712  srgbinomlem2  17774  srgbinom  17778  ringi  17793  prdsringd  17840  imasring  17847  opprring  17859  mulgass3  17865  dvrass  17918  kerf1hrm  17971  subrgunit  18026  issubrg2  18028  abvdiv  18065  islss3  18182  prdslmodd  18192  islmhm2  18261  lspsolv  18366  islbs2  18377  islbs3  18378  lbsextlem4  18384  sralmod  18410  issubassa  18548  sraassa  18549  psrbaglecl  18593  psrbagcon  18595  psrgrp  18622  psrlmod  18625  psrring  18635  psrassa  18638  ipdir  19206  ipdi  19207  ipsubdir  19209  ipsubdi  19210  ipass  19212  ipassr  19213  ipassr2  19214  ocvlss  19235  mamudm  19413  matring  19468  matassa  19469  ofco2  19476  mdetunilem1  19637  mdetunilem9  19645  mdetuni0  19646  mdetmul  19648  gsummatr01lem3  19682  iinopn  19932  subbascn  20270  nrmsep2  20372  isnrm3  20375  regsep2  20392  dnsconst  20394  dfcon2  20434  1stcelcls  20476  nllyidm  20504  dislly  20512  upxp  20638  fbasne0  20845  filss  20868  infil  20878  fsubbas  20882  filssufilg  20926  tmdcn2  21104  psmettri  21327  isxmet2d  21342  xmettri  21366  xmetres2  21376  bldisj  21413  blss2ps  21418  blss2  21419  xmstri2  21481  mstri2  21482  xmstri  21483  mstri  21484  xmstri3  21485  mstri3  21486  msrtri  21487  comet  21528  stdbdbl  21532  met2ndci  21537  ngprcan  21623  ngplcan  21624  ngpsubcan  21627  nrgdsdi  21668  nrgdsdir  21669  nlmdsdi  21684  nlmdsdir  21685  blcvx  21816  icccmplem2  21841  pi1grplem  22080  pi1cof  22090  cvsdiv  22140  cvsdivcl  22141  cphdivcl  22160  cphsubdir  22185  cphsubdi  22186  cphassr  22189  bcthlem5  22296  rrxcph  22351  volfiniun  22500  volcn  22564  itg1val2  22642  dvconst  22871  dvlip  22945  dvfsumlem4  22981  ftc1a  22989  ulmval  23335  ulmdvlem3  23357  ang180  23743  cvxcl  23910  scvxcvx  23911  sgmmul  24129  logexprlim  24153  dchrabl  24182  motgrp  24588  iscgra1  24852  cgrane1  24854  cgrane2  24855  cgrahl1  24858  cgrahl2  24859  cgracgr  24860  cgratr  24865  cgrabtwn  24867  dfcgra2  24871  sacgr  24872  f1otrge  24902  colinearalglem1  24936  colinearalg  24940  axcgrtr  24945  axlowdimlem16  24987  axeuclidlem  24992  axcontlem7  25000  eengtrkg  25015  eengtrkge  25016  wlkoniswlk  25264  constr2trl  25329  wlkdvspth  25338  erclwwlktr  25543  erclwwlkntr  25555  el2spthonot0  25599  el2wlkonotot0  25600  usg2wotspth  25612  2pthwlkonot  25613  iseupa  25693  numclwwlk5  25840  friendship  25850  grpodivdiv  25976  grpomuldivass  25977  grpopnpcan2  25981  ablodivdiv4  26019  ablonnncan  26021  ablonnncan1  26023  zerdivemp1  26162  nvmdi  26271  dipassr  26487  archiabllem2c  28512  dvrdir  28553  dvrcan5  28556  reofld  28603  pstmfval  28699  tpr2rico  28718  qqhval2lem  28785  qqhvq  28791  issiga  28933  measdivcstOLD  29046  measdivcst  29047  carsggect  29150  signsply0  29440  bnj149  29686  bnj1118  29793  bnj1128  29799  erdszelem9  29922  rescon  29969  cvmseu  29999  cvmlift2lem12  30037  elmrsubrn  30158  mclsind  30208  cgrid2  30770  segconeu  30778  btwncomim  30780  btwnswapid  30784  cgrxfr  30822  btwnxfr  30823  colineardim1  30828  brofs2  30844  brifs2  30845  idinside  30851  endofsegid  30852  btwnconn1lem7  30860  btwnconn1lem11  30864  btwnconn1  30868  segcon2  30872  seglemin  30880  segletr  30881  btwnsegle  30884  colinbtwnle  30885  broutsideof2  30889  broutsideof3  30893  outsidele  30899  fvray  30908  fvline  30911  linerflx1  30916  ellines  30919  ivthALT  30991  poimirlem32  31972  ftc1anc  32025  sdclem1  32072  sstotbnd2  32106  zerdivemp1x  32194  isdrngo2  32197  iscringd  32232  lsmsat  32574  lfladdcl  32637  lflnegcl  32641  lflvscl  32643  lshpkrlem4  32679  lshpkrlem6  32681  ldualgrplem  32711  lduallmodlem  32718  latmassOLD  32795  latm12  32796  latm32  32797  latmrot  32798  latmmdiN  32800  latmmdir  32801  omlfh1N  32824  omlfh3N  32825  cvlexchb1  32896  cvlexch3  32898  cvlexch4N  32899  cvlatexchb1  32900  cvlsupr2  32909  hlatjass  32935  hlatj12  32936  hlatj32  32937  cvratlem  32986  cvrat  32987  atcvrj0  32993  cvrat2  32994  atltcvr  33000  atexchltN  33006  cvrat3  33007  cvrat4  33008  3dimlem3  33026  3dimlem3OLDN  33027  3at  33055  2atneat  33080  llncmp  33087  2at0mat0  33090  2atmat0  33091  lplnnle2at  33106  llncvrlpln  33123  lplncmp  33127  lplnexllnN  33129  2llnjaN  33131  4atlem11  33174  lplncvrlvol  33181  lvolcmp  33182  2atm2atN  33350  elpaddatriN  33368  paddasslem9  33393  paddass  33403  padd12N  33404  paddssw2  33409  paddss  33410  pmodlem2  33412  pmodN  33415  pmapjlln1  33420  atmod1i1  33422  atmod1i2  33424  pexmidlem2N  33536  pexmidlem6N  33540  pl42N  33548  lhpm0atN  33594  lautlt  33656  lautcvr  33657  lautj  33658  lautm  33659  ltrneq2  33713  cdlemc3  33759  cdlemc4  33760  cdlemd1  33764  cdleme1b  33792  cdleme1  33793  cdleme2  33794  cdleme3e  33798  cdlemefr27cl  33970  cdlemefs27cl  33980  cdleme42mN  34054  cdlemftr2  34133  trljco  34307  tgrpgrplem  34316  tendoplass  34350  tendodi1  34351  tendodi2  34352  cdlemk36  34480  erngdvlem3  34557  erngdvlem3-rN  34565  tendospdi1  34588  dvalveclem  34593  dialss  34614  dvhvaddass  34665  dvhopvsca  34670  dvhlveclem  34676  diblss  34738  diclss  34761  dihmeetlem12N  34886  dihmeetlem15N  34889  dihmeetlem16N  34890  dihmeetlem17N  34891  dihmeetlem18N  34892  dihmeetlem19N  34893  dvh4dimN  35015  lpolvN  35054  lclkr  35101  lclkrs  35107  lcfr  35153  irrapxlem6  35671  jm2.26lem3  35856  dgrsub2  35994  mpaadgr  36020  mendring  36058  mendlmod  36059  mendassa  36060  relexpmulg  36302  iunrelexpmin2  36304  relexpxpmin  36309  fmuldfeq  37661  stoweidlem43  37904  stoweidlem52  37913  stoweidlem53  37914  stoweidlem56  37917  stoweidlem57  37918  nbfusgrlevtxm2  39452  upgr1wlkwlk  39651  wlkOnwlk  39662  upgrspths1wlk  39697  usgfis  39811  usgfisALT  39815  copissgrp  39861  cznrng  40010  funcringcsetcALTV2lem9  40099  funcringcsetclem9ALTV  40122  ply1ass23l  40227  linccl  40260  lincext1  40300  lincext3  40302  lincresunit2  40324
  Copyright terms: Public domain W3C validator