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

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

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 1006 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 467 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simplr2  1048  simprr2  1054  simp1r2  1102  simp2r2  1108  simp3r2  1114  3anandis  1366  wereu  4849  fpr2g  6140  isopolem  6251  fr3nr  6620  frfi  7825  intrnfi  7939  fisupcl  7994  cnfcomlem  8212  ackbij1lem15  8671  cofsmo  8706  sornom  8714  fpwwe2lem5  9066  dedekindle  9805  supmul1  10583  eluzuzle  11174  xlesubadd  11556  elioc2  11704  elico2  11705  elicc2  11706  fseq1p1m1  11875  fz0fzelfz0  11903  swrdsbslen  12806  swrdspsleq  12807  ccatswrd  12814  swrdswrdlem  12817  tanadd  14220  dvds2ln  14332  cshwsidrepsw  15063  ressress  15186  f1ovscpbl  15431  mreexexlem4d  15552  mreexexd  15553  iscatd2  15586  2oppccomf  15629  issubc3  15753  fthmon  15831  fuccocl  15868  fucidcl  15869  invfuc  15878  initoeu2lem0  15907  initoeu2lem1  15908  curf2cl  16115  yonedalem4c  16161  yonedalem3  16164  pospo  16218  latjle12  16307  latjlej1  16310  latnlej2  16316  latlem12  16323  latmlem1  16326  latledi  16334  latjass  16340  latj12  16341  latj32  16342  latj13  16343  latj31  16344  latjrot  16345  latjjdi  16348  latjjdir  16349  latdisdlem  16434  prdsmndd  16568  frmdmnd  16642  grpsubrcan  16734  grpsubadd  16741  grpaddsubass  16743  grpsubsub4  16746  grppnpcan2  16747  grpnpncan  16748  mulgnndir  16779  mulgnn0dir  16780  mulgdir  16782  mulgnnass  16785  mulgnn0ass  16786  mulgass  16787  mulgsubdir  16788  pwsmulg  16799  issubg2  16831  eqgval  16865  qusgrp  16871  galcan  16957  gacan  16958  oppgmnd  17004  symggrp  17040  fvcosymgeq  17069  pmtrprfv  17093  psgnunilem3  17136  cmn32  17447  cmn12  17449  abladdsub  17456  mulgdi  17466  mulgsubdi  17469  dprdss  17661  dprdz  17662  dprdf1o  17664  dprdsn  17668  dprd2da  17674  dmdprdsplit  17679  ablfac1b  17702  pgpfac1lem5  17711  srgi  17744  srgbinom  17777  ringi  17792  prdsringd  17839  opprring  17858  mulgass3  17864  dvrass  17917  subrgunit  18025  issubrg2  18027  abvdiv  18064  lsssn0  18170  islss3  18181  prdslmodd  18191  islmhm2  18260  lspsolv  18365  islbs2  18376  islbs3  18377  lbsextlem4  18383  sralmod  18409  issubassa  18547  sraassa  18548  psrbaglesupp  18591  psrbaglecl  18592  psrbagcon  18594  psrgrp  18621  psrlmod  18624  psrring  18634  psrassa  18637  psgndiflemB  19166  ipdir  19204  ipdi  19205  ipsubdir  19207  ipsubdi  19208  ipass  19210  ipassr  19211  ipassr2  19212  isphld  19219  ocvlss  19233  mamudm  19411  matring  19466  matassa  19467  ofco2  19474  ma1repveval  19594  mdetunilem1  19635  mdetunilem9  19643  chpscmatgsumbin  19866  iinopn  19930  restopnb  20189  subbascn  20268  nrmsep2  20370  isnrm3  20373  regsep2  20390  dnsconst  20392  dfcon2  20432  1stcelcls  20474  dislly  20510  ptuni2  20589  tx1stc  20663  0nelfb  20844  infil  20876  fsubbas  20880  filssufilg  20924  hauspwpwf1  21000  cnextcn  21080  tmdcn2  21102  ustuqtoplem  21252  utopsnneiplem  21260  psmettri  21325  isxmet2d  21340  xmettri  21364  xmetres2  21374  bldisj  21411  blss2ps  21416  blss2  21417  xmstri2  21479  mstri2  21480  xmstri  21481  mstri  21482  xmstri3  21483  mstri3  21484  msrtri  21485  comet  21526  stdbdbl  21530  met2ndci  21535  ngprcan  21621  ngplcan  21622  ngpsubcan  21625  nrgdsdi  21666  nrgdsdir  21667  nlmdsdi  21682  nlmdsdir  21683  blcvx  21814  icoopnst  21965  pi1grplem  22078  cvsdiv  22138  cvsdivcl  22139  cphdivcl  22158  cphsubdir  22183  cphsubdi  22184  tchcph  22209  bcthlem5  22294  volfiniun  22498  volcn  22562  itg1val2  22640  dvconst  22869  dvlip  22943  ftc1a  22987  ulmval  23333  ulmdvlem3  23355  ang180  23741  cvxcl  23908  scvxcvx  23909  sgmmul  24127  dchrabl  24180  motgrp  24586  iscgra1  24850  cgrane1  24852  cgrane3  24854  cgrahl1  24856  cgrahl2  24857  cgracgr  24858  cgratr  24863  cgrabtwn  24865  cgrahl  24866  dfcgra2  24869  sacgr  24870  f1otrge  24900  colinearalglem1  24934  axcgrtr  24943  axeuclidlem  24990  axcontlem3  24994  axcontlem4  24995  axcontlem7  24998  eengtrkg  25013  eengtrkge  25014  isspthonpth  25312  wlkdvspth  25336  clwlkfoclwwlk  25571  el2spthonot0  25597  el2wlkonotot0  25598  usg2wotspth  25610  2spontn0vne  25613  rusgranumwlks  25682  rusgranumwwlkg  25685  iseupa  25691  3vfriswmgra  25731  frgrareggt1  25842  grpomuldivass  25975  grponpncan  25981  grpodiveq  25982  ablomuldiv  26015  ablodivdiv4  26017  ablonnncan1  26021  nvmdi  26269  nvsubadd  26274  dipassr  26485  archiabllem2c  28519  dvrdir  28561  dvrcan5  28564  reofld  28611  pstmfval  28707  qqhval2lem  28793  qqhvq  28799  measdivcstOLD  29054  measdivcst  29055  carsggect  29158  bnj1098  29603  bnj149  29694  bnj1118  29801  erdszelem9  29930  rescon  29977  cvmseu  30007  cvmlift2lem10  30043  cvmlift2lem12  30045  elmrsubrn  30166  mclsind  30216  frrlem4  30524  cgrid2  30775  segconeu  30783  btwncomim  30785  btwnswapid  30789  trisegint  30800  cgrxfr  30827  brofs2  30849  endofsegid  30857  btwnconn2  30874  seglemin  30885  segletr  30886  btwnsegle  30889  colinbtwnle  30890  broutsideof2  30894  btwnoutside  30897  broutsideof3  30898  outsideoftr  30901  outsidele  30904  fvray  30913  fvline  30916  ellines  30924  broucube  31938  ftc1anc  31989  sdclem1  32036  sstotbnd2  32070  iscringd  32196  lsmsat  32543  lfladdcl  32606  lflnegcl  32610  lflvscl  32612  eqlkr  32634  lshpkrlem4  32648  lshpkrlem6  32650  ldualgrplem  32680  lduallmodlem  32687  latmassOLD  32764  latm12  32765  latm32  32766  latmrot  32767  latmmdiN  32769  latmmdir  32770  omlfh1N  32793  omlfh3N  32794  cvrnbtwn2  32810  cvlexchb1  32865  cvlsupr2  32878  hlatjass  32904  hlatj12  32905  hlatj32  32906  cvrat  32956  cvrat2  32963  atltcvr  32969  atexchltN  32975  cvrat3  32976  cvrat4  32977  atbtwnexOLDN  32981  atbtwnex  32982  3dimlem3  32995  3dimlem3OLDN  32996  3at  33024  2atneat  33049  llncmp  33056  2at0mat0  33059  2atmat0  33060  llncvrlpln  33092  lplncmp  33096  2llnjaN  33100  4atlem11  33143  lplncvrlvol  33150  lvolcmp  33151  2atm2atN  33319  elpaddatriN  33337  paddasslem8  33361  paddass  33372  padd12N  33373  paddssw2  33378  paddss  33379  pmod1i  33382  pmodN  33384  pmapjlln1  33389  atmod1i1  33391  atmod1i2  33393  pexmidlem2N  33505  pl42lem2N  33514  pl42lem3N  33515  pl42lem4N  33516  pl42N  33517  lhpm0atN  33563  lautlt  33625  lautcvr  33626  lautj  33627  lautm  33628  ltrneq2  33682  cdlemd1  33733  cdleme1b  33761  cdleme1  33762  cdleme2  33763  cdleme3e  33767  cdlemefr27cl  33939  cdlemefs27cl  33949  cdleme42ke  34021  cdleme42mN  34023  cdlemf2  34098  cdlemftr2  34102  trljco  34276  tgrpgrplem  34285  tendoplass  34319  tendodi1  34320  tendodi2  34321  cdlemk34  34446  cdlemk36  34449  erngdvlem3-rN  34534  tendospdi1  34557  dialss  34583  dvhvaddass  34634  dvhopvsca  34639  dvhlveclem  34645  diblss  34707  diclss  34730  diclspsn  34731  cdlemn11pre  34747  dihmeetlem12N  34855  dihmeetlem16N  34859  dihmeetlem17N  34860  dihmeetlem18N  34861  dvh4dimN  34984  lpolconN  35024  dochpolN  35027  lclkr  35070  lclkrs  35076  lcfr  35122  irrapxlem6  35641  jm2.26lem3  35826  dgrsub2  35964  mpaaroot  35991  mendring  36028  mendlmod  36029  mendassa  36030  relexpmulg  36272  iunrelexpmin2  36274  relexpxpmin  36279  rfcnpre3  37327  fmuldfeq  37601  stoweidlem43  37844  stoweidlem52  37853  stoweidlem53  37854  stoweidlem56  37857  stoweidlem57  37858  stoweidlem60  37861  iccpartigtl  38607  iccelpart  38617  ltsubsubaddltsub  38902  subgruhgredgd  39130  copissgrp  39428  cznrng  39577  funcringcsetcALTV2lem9  39666  funcringcsetclem9ALTV  39689  ldepsprlem  39887  lincresunit3  39896  lincreslvec3  39897
  Copyright terms: Public domain W3C validator