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

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

Proof of Theorem simpl2
StepHypRef Expression
1 simp2 995 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 463 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:  simpll2  1034  simprl2  1040  simp1l2  1088  simp2l2  1094  simp3l2  1100  3anandirs  1329  rspc3ev  3148  brcogw  5084  weniso  6151  ofmpteq  6457  tfisi  6592  mpt2sn  6790  smogt  6956  smorndom  6957  omeulem1  7149  nnmord  7199  nnmword  7200  difsnen  7518  enfixsn  7545  mapunen  7605  ac6sfi  7679  ordiso2  7855  wemaplem2  7887  wemapso  7891  wemapso2lem  7893  en2eqpr  8298  acndom  8345  infmap2  8511  cflim2  8556  cfsmolem  8563  coftr  8566  fin23lem26  8618  isf32lem9  8654  fin1a2lem9  8701  fin1a2lem10  8702  ac6num  8772  gchdomtri  8918  canth4  8936  gchpwdom  8959  gruima  9091  grudomon  9106  prn0  9278  distrlem4pr  9315  prlem934  9322  addcan  9675  addcan2  9676  ltmul1a  10308  supmul1  10424  uzsupss  11093  xaddass  11362  xleadd1a  11366  xlesubadd  11376  xmulass  11400  xlemul2a  11402  xadddilem  11407  xadddi  11408  ixxdisj  11465  ixxun  11466  ixxlb  11472  icoshftf1o  11564  icodisj  11566  lincmb01cmp  11584  iccf1o  11585  ssfzoulel  11805  modaddmulmod  11956  ltexp2a  12120  leexp2  12123  ltexp2r  12125  exple1  12128  expnlbnd2  12199  ccatass  12514  ccatopth  12606  swrdccatin12lem2a  12621  repswccat  12668  2cshw  12692  repsco  12716  s2f1o  12775  limsupgle  13302  limsupgre  13306  addcn2  13418  mulcn2  13420  dvdsval2  13991  dvdsadd2b  14030  dvdsmod  14045  oexpneg  14051  sadass  14123  gcdass  14185  rplpwr  14196  rppwr  14197  coprmdvds2  14246  rpmulgcd2  14248  rpexp  14263  rpdvds  14267  prmdiveq  14318  odzdvds  14324  coprimeprodsq2  14336  pythagtriplem3  14344  pythagtriplem4  14345  pcdvdsb  14394  vdwnnlem1  14515  0ram  14540  ramz2  14544  ramub1lem1  14546  mremre  15011  mrieqv2d  15046  lubss  15868  lubun  15870  clatleglb  15873  clatglbss  15874  mrelatglb  15931  isnsgrp  16032  issubmnd  16065  gsumccat  16126  frmdss2  16148  nmzsubg  16359  ghmnsgima  16407  gsmsymgreqlem1  16572  psgnunilem4  16639  odmodnn0  16681  odnncl  16686  odmod  16687  oddvds  16688  odeq  16691  odmulgid  16693  odmulgeq  16696  odbezout  16697  odf1o1  16709  odf1o2  16710  odngen  16714  gexdvdsi  16720  pgpfi1  16732  odcau  16741  subgslw  16753  fislw  16762  lsmless1x  16781  lsmless2x  16782  lsmsubm  16790  lsmmod  16810  lsmmod2  16811  efgsfo  16874  odadd1  16971  odadd2  16972  odadd  16973  lsmcomx  16979  prdscmnd  16984  gsumconst  17070  srg1zr  17293  csrgbinom  17310  ring1eq0  17351  mulgass2  17360  cntzsubr  17574  isabvd  17582  0lmhm  17799  lmhmvsca  17804  reslmhm2b  17813  pwssplit1  17818  pwssplit2  17819  pwssplit3  17820  lbspss  17841  lspsnat  17904  lidldvgen  18016  issubassa  18086  evlsval2  18302  coe1subfv  18420  coe1sclmul  18436  coe1sclmul2  18438  xrsdsreclblem  18577  cssmre  18815  obs2ss  18851  uvcresum  18913  frlmsslsp  18916  frlmup4  18921  lindff1  18940  f1lindf  18942  lsslindf  18950  islindf4  18958  mpt2matmul  19033  mamutpos  19045  scmatscmide  19094  mavmulsolcl  19138  mulmarep1gsum2  19161  mdetdiaglem  19185  mdetdiag  19186  mdetunilem1  19199  mdetunilem3  19201  mdetunilem9  19207  maducoeval2  19227  madurid  19231  slesolinvbi  19268  cramerimplem1  19270  cramerlem1  19274  cramer  19278  cpmatel2  19299  m2cpm  19327  m2pmfzmap  19333  m2cpminvid2lem  19340  m2cpminvid2  19341  decpmatmul  19358  pmatcollpw1lem2  19361  pmatcollpw1  19362  pmatcollpw2lem  19363  pmatcollpwfi  19368  pm2mpcl  19383  mply1topmatcl  19391  mp2pm2mplem2  19393  mp2pm2mplem4  19395  mp2pm2mplem5  19396  mp2pm2mp  19397  pm2mpghmlem2  19398  pm2mpghmlem1  19399  chfacfisfcpmat  19441  topssnei  19711  cnconst2  19870  cnpresti  19875  cnprest2  19877  cnpdis  19880  cnt0  19933  cnt1  19937  cnhaus  19941  sscmp  19991  hauscmp  19993  cnconn  20008  uncon  20015  finlocfin  20106  comppfsc  20118  kgen2ss  20141  ptpjopn  20198  prdstopn  20214  ptrescn  20225  qtopss  20301  kqfvima  20316  fbssint  20424  fbasrn  20470  filuni  20471  fmss  20532  rnelfm  20539  fmufil  20545  fmco  20547  flimss2  20558  flimss1  20559  flimrest  20569  cnpflf2  20586  flfcnp  20590  supnfcls  20606  fclsss1  20608  fclsss2  20609  isfcf  20620  subgntr  20690  opnsubg  20691  cldsubg  20694  ghmcnp  20698  ustuqtop1  20829  bldisj  20986  blgt0  20987  bl2in  20988  blss2ps  20991  blss2  20992  blssps  21012  blss  21013  xmetresbl  21025  lpbl  21091  blcld  21093  stdbdmopn  21106  metcnp3  21128  metcnp  21129  metcnp2  21130  txmetcnp  21135  blval2  21163  nmoix  21321  nmoi2  21322  nmotri  21331  metdsge  21438  metdseq0  21443  iocopnst  21525  xrhmeo  21531  nmhmcn  21688  cphsqrtcl2  21718  cphsqrtcl3  21719  pjth  21939  ovoliunlem2  21999  volun  22040  mbfimaopn2  22149  iblconst  22309  limcvallem  22360  dvfval  22386  dvcnp2  22408  dvcn  22409  deg1mul3le  22602  deg1tmle  22603  dvdsq1p  22646  ig1peu  22657  ig1pdvds  22662  ply1term  22686  coeid3  22722  dgrmulc  22753  dvply1  22765  aaliou2  22821  efcvx  22929  tanord  23010  eflogeq  23074  logdivlti  23092  logccv  23131  recxpcl  23143  cxplea  23164  cxpeq  23218  ang180  23264  isosctrlem2  23269  cxp2lim  23423  amgm  23437  muval1  23524  dvdssqf  23529  mumullem2  23571  mumul  23572  bcmono  23669  lgsneg  23711  lgsdilem  23714  lgsdirprm  23721  lgsdir  23722  lgsdi  23724  lgsne0  23725  brbtwn2  24329  colinearalglem1  24330  colinearalg  24334  axcgrtr  24339  axsegconlem8  24348  axsegconlem9  24349  axsegconlem10  24350  axcontlem2  24389  axcontlem10  24397  cyclispthon  24754  wwlknext  24845  clwlkisclwwlklem0  24909  erclwwlksym  24935  eleclclwwlknlem2  24939  erclwwlkneqlen  24945  erclwwlknsym  24947  vdgrfval  25016  nbhashuvtx1  25036  usgreghash2spot  25190  extwwlkfablem2  25199  numclwwlk3lem  25229  frgraregord13  25240  gxcom  25388  gxnn0add  25393  nvmul0or  25664  ipval2lem2  25731  ipval2lem5  25737  lnoadd  25790  lnosub  25791  lnomul  25792  shless  26394  shlej1  26395  kbmul  26990  homco2  27012  kbass2  27152  eliccelico  27741  elicoelioo  27742  iocinioc2  27743  iocinif  27745  difioo  27746  xrge0adddir  27835  xrge0npcan  27837  isarchi2  27882  archiabl  27895  rhmdvdsr  27962  pstmfval  28029  fmcncfil  28067  zrhnm  28103  qqhnm  28124  nexple  28158  volfiniune  28358  dya2iocnrect  28408  probinc  28543  cndprob01  28557  signswmnd  28697  cvmsss2  28908  cvmlift2lem10  28946  binomrisefac  29330  br6  29352  funsseq  29364  frrlem4  29555  cgrtriv  29805  5segofs  29809  btwnouttr2  29825  btwnxfr  29859  lineext  29879  btwnconn1lem13  29902  brsegle2  29912  nn0prpwlem  30306  blbnd  30449  ismtyima  30465  rrndstprj2  30493  ghomdiv  30512  grpokerinj  30513  diophrw  30857  eldioph2lem1  30858  diophrex  30874  rencldnfi  30920  pellexlem2  30931  pellqrexplicit  30978  infmrgelbi  30979  pellfundglb  30986  pellfund14gap  30988  rmxycomplete  31018  congadd  31069  acongeq  31086  jm2.19  31101  jm2.23  31104  jm2.20nn  31105  jm2.27  31116  jm3.1  31128  lnmepi  31197  lmhmlnmsplit  31199  hbtlem2  31241  dgraa0p  31266  idomrootle  31320  hashgcdlem  31325  proot1hash  31328  iocunico  31346  iocinico  31347  lcmass  31386  rfcnnnub  31578  snunioo2  31710  iccintsng  31729  climsuse  31780  lptre2pt  31812  limcleqr  31816  0ellimcdiv  31821  dvnprodlem1  31909  volioc  31937  stoweidlem17  31965  stoweidlem19  31967  stoweidlem20  31968  stoweidlem22  31970  stoweidlem28  31976  stoweidlem34  31982  stoweidlem44  31992  stoweidlem60  32008  wallispilem3  32015  fourierdlem42  32097  fourierdlem48  32103  fourierdlem51  32106  fourierdlem54  32109  fourierdlem74  32129  fourierdlem77  32132  fourierdlem87  32142  fourierdlem97  32152  oexpnegALTV  32519  oexpnegnz  32520  repswpfx  32611  eluzge0nn0  32650  fzoopth  32660  rmsupp0  33161  rmsuppss  33163  lincresunit3lem3  33275  lincresunit3lem2  33281  lindssnlvec  33287  fdivmptf  33362  refdivmptf  33363  elbigolo1  33378  bnj517  34290  lsatfixedN  35147  lssat  35154  lshpkrlem4  35251  cvrcon3b  35415  atlen0  35448  atcvreq0  35452  atnle  35455  atlatmstc  35457  atlatle  35458  cvlcvr1  35477  hlsupr2  35524  hlrelat2  35540  cvrexchlem  35556  lnnat  35564  atcvrj2b  35569  3dimlem3  35598  3dim1  35604  1cvrjat  35612  llni  35645  llni2  35649  llnexatN  35658  2llnmat  35661  lplni  35669  2atnelpln  35681  llncvrlpln2  35694  2llnmj  35697  lplnexatN  35700  lplnexllnN  35701  2llnm3N  35706  lvoli  35712  lvoli3  35714  lvolnle3at  35719  islvol2aN  35729  4atlem4a  35736  4atlem4b  35737  4atlem11  35746  lplncvrlvol2  35752  2lplnmj  35759  islinei  35877  linepmap  35912  lnjatN  35917  lncvrat  35919  lncmp  35920  elpaddn0  35937  elpaddatriN  35940  elpaddat  35941  paddcom  35950  paddss2  35955  paddss12  35956  paddasslem4  35960  paddasslem9  35965  paddasslem10  35966  pmodl42N  35988  pmapjoin  35989  llnmod1i2  35997  polcon2bN  36057  pclfinclN  36087  poml4N  36090  poml6N  36092  osumcllem1N  36093  osumcllem2N  36094  osumcllem11N  36103  osumclN  36104  pmapojoinN  36105  pexmidlem2N  36108  pexmidlem3N  36109  pexmidlem4N  36110  pexmidlem6N  36112  pexmidlem7N  36113  pl42lem2N  36117  pl42lem3N  36118  pl42lem4N  36119  pl42N  36120  lhprelat3N  36177  4atex  36213  lauteq  36232  lautco  36234  ltrncoidN  36265  ltrneq2  36285  ltrnideq  36313  trlnle  36324  trlval3  36325  cdlemc  36335  cdlemd9  36344  cdlemd  36345  cdleme21j  36475  cdleme21  36476  cdleme29ex  36513  cdlemefr27cl  36542  cdlemefs27cl  36552  cdleme32d  36583  cdleme32f  36585  cdleme35h2  36596  cdleme40m  36606  cdleme17d3  36635  cdleme48fvg  36639  cdlemeg46fvcl  36645  cdlemeg46fgN  36673  cdleme48fgv  36677  cdleme50trn3  36692  cdlemb3  36745  cdlemg8  36770  cdlemg11a  36776  cdlemg15a  36794  cdlemg15  36795  cdlemg16  36796  cdlemg16z  36798  cdlemg17dN  36802  cdlemg24  36827  cdlemg37  36828  cdlemg29  36844  cdlemg33b  36846  cdlemg38  36854  cdlemg40  36856  trlco  36866  cdlemg44b  36871  ltrncom  36877  trljco  36879  tendococl  36911  tendoplcl  36920  tendoplcom  36921  cdlemj2  36961  tendoid0  36964  tendo1ne0  36967  cdlemk25-3  37043  cdlemk36  37052  cdlemkid4  37073  cdlemk19x  37082  cdlemk53  37096  cdlemk56  37110  cdleml5N  37119  tendospcanN  37163  cdlemm10N  37258  dihord6apre  37396  dihord  37404  dihmeetlem1N  37430  dihglblem2N  37434  dihmeetlem2N  37439  dihmeetbN  37443  dihmeetlem5  37448  dihmeetlem6  37449  dihmeetlem7N  37450  dihmeetlem10N  37456  dihmeetlem12N  37458  dihmeetlem16N  37462  dihmeetlem17N  37463  dihmeetlem18N  37464  dihmeetALTN  37467  dihlspsnssN  37472  dvh3dim2  37588  dvh3dim3N  37589  lcfrlem16  37698  mapdrvallem2  37785  mapdh8ad  37919  hgmapvvlem3  38068  relexpxpmin  38244
  Copyright terms: Public domain W3C validator