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

Theorem simpl2 959
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 956 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 451 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simpll2  995  simprl2  1001  simp1l2  1049  simp2l2  1055  simp3l2  1061  3anandirs  1284  rspc3ev  2894  tfisi  4649  weniso  5852  smogt  6384  smorndom  6385  omeulem1  6580  nnmord  6630  nnmword  6631  difsnen  6944  mapunen  7030  ac6sfi  7101  ordiso2  7230  wemaplem2  7262  wemapso  7266  en2eqpr  7637  acndom  7678  infmap2  7844  cflim2  7889  cfsmolem  7896  coftr  7899  fin23lem26  7951  isf32lem9  7987  fin1a2lem9  8034  fin1a2lem10  8035  ac6num  8106  gchdomtri  8251  canth4  8269  gchpwdom  8296  gruima  8424  grudomon  8439  prn0  8613  distrlem4pr  8650  prlem934  8657  addcan  8996  addcan2  8997  ltmul1a  9605  ledivmulOLD  9630  supmul1  9719  uzsupss  10310  xaddass  10569  xleadd1a  10573  xlesubadd  10583  xmulass  10607  xlemul2a  10609  xadddilem  10614  xadddi  10615  ixxdisj  10671  ixxun  10672  ixxlb  10678  icoshftf1o  10759  icodisj  10761  lincmb01cmp  10777  iccf1o  10778  ltexp2a  11153  leexp2  11156  ltexp2r  11158  exple1  11161  expnlbnd2  11232  ccatass  11436  ccatopth  11462  limsupgle  11951  limsupgre  11955  addcn2  12067  mulcn2  12069  dvdsval2  12534  dvdsadd2b  12571  dvdsmod  12585  oexpneg  12590  sadass  12662  gcdass  12724  rplpwr  12735  rppwr  12736  coprmdvds2  12782  rpmulgcd2  12784  rpexp  12799  rpdvds  12803  prmdiveq  12854  odzdvds  12860  coprimeprodsq2  12863  pythagtriplem3  12871  pythagtriplem4  12872  pcdvdsb  12921  vdwnnlem1  13042  0ram  13067  ramz2  13071  ramub1lem1  13073  mremre  13506  mrieqv2d  13541  lubss  14225  lubun  14227  clatleglb  14230  clatglbss  14231  mrelatglb  14287  issubmnd  14401  gsumccat  14464  frmdss2  14485  nmzsubg  14658  ghmnsgima  14706  odmodnn0  14855  odnncl  14860  odmod  14861  oddvds  14862  odeq  14865  odmulgid  14867  odmulgeq  14870  odbezout  14871  odf1o1  14883  odf1o2  14884  odngen  14888  gexdvdsi  14894  pgpfi1  14906  odcau  14915  subgslw  14927  fislw  14936  lsmless1x  14955  lsmless2x  14956  lsmsubm  14964  lsmmod  14984  lsmmod2  14985  efgsfo  15048  odadd1  15140  odadd2  15141  odadd  15142  lsmcomx  15148  prdscmnd  15153  gsumconst  15209  rng1eq0  15379  mulgass2  15387  cntzsubr  15577  isabvd  15585  0lmhm  15797  lmhmvsca  15802  reslmhm2b  15811  lbspss  15835  lspsnat  15898  lidldvgen  16007  issubassa  16064  coe1subfv  16343  coe1sclmul  16358  coe1sclmul2  16360  xrsdsreclblem  16417  cssmre  16593  obs2ss  16629  topssnei  16861  cnconst2  17011  cnpresti  17016  cnprest2  17018  cnpdis  17021  cnt0  17074  cnt1  17078  cnhaus  17082  sscmp  17132  hauscmp  17134  cnconn  17148  uncon  17155  kgen2ss  17250  ptpjopn  17306  prdstopn  17322  ptrescn  17333  qtopss  17406  kqfvima  17421  fbssint  17533  fbasrn  17579  filuni  17580  fmss  17641  rnelfm  17648  fmufil  17654  fmco  17656  flimss2  17667  flimss1  17668  flimrest  17678  cnpflf2  17695  flfcnp  17699  supnfcls  17715  fclsss1  17717  fclsss2  17718  isfcf  17729  subgntr  17789  opnsubg  17790  cldsubg  17793  ghmcnp  17797  bldisj  17955  blgt0  17956  bl2in  17957  blss2  17959  blss  17972  xmetresbl  17983  lpbl  18049  blcld  18051  stdbdmopn  18064  metcnp3  18086  metcnp  18087  metcnp2  18088  txmetcnp  18093  nmoix  18238  nmoi2  18239  nmotri  18248  metdsge  18353  metdseq0  18358  iocopnst  18438  xrhmeo  18444  nmhmcn  18601  cphsqrcl2  18622  cphsqrcl3  18623  pjth  18803  ovoliunlem2  18862  volun  18902  mbfimaopn2  19012  iblconst  19172  limcvallem  19221  dvfval  19247  dvcnp2  19269  dvcn  19270  evlsval2  19404  deg1mul3le  19502  deg1tmle  19503  dvdsq1p  19546  ig1peu  19557  ig1pdvds  19562  ply1term  19586  coeid3  19622  dgrmulc  19652  dvply1  19664  aaliou2  19720  efcvx  19825  tanord  19900  eflogeq  19955  logdivlti  19971  logccv  20010  recxpcl  20022  cxplea  20043  cxpeq  20097  ang180  20112  isosctrlem2  20119  cxp2lim  20271  amgm  20285  muval1  20371  dvdssqf  20376  mumullem2  20418  mumul  20419  bcmono  20516  lgsneg  20558  lgsdilem  20561  lgsdirprm  20568  lgsdir  20569  lgsdi  20571  lgsne0  20572  gxcom  20936  gxnn0add  20941  nvmul0or  21210  ipval2lem2  21277  ipval2lem5  21283  lnoadd  21336  lnosub  21337  lnomul  21338  shless  21938  shlej1  21939  kbmul  22535  homco2  22557  kbass2  22697  eliccelico  23270  elicoelioo  23271  iocinioc2  23272  iocinif  23274  difioo  23275  xrge0adddir  23332  xrge0npcan  23333  probinc  23624  cndprob01  23638  cvmsss2  23805  cvmlift2lem10  23843  vdgrfval  23889  br6  24114  funsseq  24125  frrlem4  24284  brbtwn2  24533  colinearalglem1  24534  colinearalg  24538  axcgrtr  24543  axsegconlem8  24552  axsegconlem9  24553  axsegconlem10  24554  axcontlem2  24593  axcontlem10  24601  cgrtriv  24625  5segofs  24629  btwnouttr2  24645  btwnxfr  24679  lineext  24699  btwnconn1lem13  24722  brsegle2  24732  sndw  25100  mapmapmap  25148  iscst4  25177  cmprtr  25396  rltrran  25414  rltrooo  25415  cnrsfin  25525  cnrscoa  25526  efilcp  25552  fgsb2  25555  cmptdst  25568  cmptdst2  25571  limptlimpr2lem2  25575  flfnei2  25577  islimrs3  25581  usinuniopb  25594  lvsovso  25626  addcanri  25666  negveud  25668  mulmulvec  25687  distmlva  25688  distsava  25689  isder  25707  iepiclem  25823  tartarmap  25888  indcls2  25996  lppotos  26144  pdiveql  26168  nn0prpwlem  26238  finlocfin  26299  comppfsc  26307  blbnd  26511  ismtyima  26527  rrndstprj2  26555  ghomdiv  26574  grpokerinj  26575  ofmpteq  26797  diophrw  26838  eldioph2lem1  26839  diophrex  26855  rencldnfi  26904  pellexlem2  26915  pellqrexplicit  26962  infmrgelbi  26963  pellfundglb  26970  pellfund14gap  26972  rmxycomplete  27002  congadd  27053  acongeq  27070  jm2.19  27086  jm2.23  27089  jm2.20nn  27090  jm2.27  27101  jm3.1  27113  lnmepi  27183  lmhmlnmsplit  27185  pwssplit1  27188  pwssplit2  27189  pwssplit3  27190  uvcresum  27242  frlmsslsp  27248  frlmup4  27253  enfixsn  27257  lindff1  27290  f1lindf  27292  lsslindf  27300  islindf4  27308  hbtlem2  27328  dgraa0p  27354  psgnunilem4  27420  idomrootle  27511  hashgcdlem  27516  proot1hash  27519  rfcnnnub  27707  climsuse  27734  stoweidlem19  27768  stoweidlem20  27769  stoweidlem22  27771  stoweidlem28  27777  stoweidlem34  27783  stoweidlem44  27793  stoweidlem51  27800  stoweidlem60  27809  wallispilem3  27816  s2f1o  28091  bnj517  28917  lubunNEW  29163  lsatfixedN  29199  lssat  29206  lshpkrlem4  29303  op0cl  29374  cvrcon3b  29467  atlen0  29500  atcvreq0  29504  atnle  29507  atlatmstc  29509  atlatle  29510  cvlcvr1  29529  hlsupr2  29576  hlrelat2  29592  cvrexchlem  29608  lnnat  29616  atcvrj2b  29621  3dimlem3  29650  3dim1  29656  1cvrjat  29664  llni  29697  llni2  29701  llnexatN  29710  2llnmat  29713  lplni  29721  2atnelpln  29733  llncvrlpln2  29746  2llnmj  29749  lplnexatN  29752  lplnexllnN  29753  2llnm3N  29758  lvoli  29764  lvoli3  29766  lvolnle3at  29771  islvol2aN  29781  4atlem4a  29788  4atlem4b  29789  4atlem11  29798  lplncvrlvol2  29804  2lplnmj  29811  islinei  29929  linepmap  29964  lnjatN  29969  lncvrat  29971  lncmp  29972  elpaddn0  29989  elpaddatriN  29992  elpaddat  29993  paddcom  30002  paddss2  30007  paddss12  30008  paddasslem4  30012  paddasslem9  30017  paddasslem10  30018  pmodl42N  30040  pmapjoin  30041  llnmod1i2  30049  polcon2bN  30109  pclfinclN  30139  poml4N  30142  poml6N  30144  osumcllem1N  30145  osumcllem2N  30146  osumcllem11N  30155  osumclN  30156  pmapojoinN  30157  pexmidlem2N  30160  pexmidlem3N  30161  pexmidlem4N  30162  pexmidlem6N  30164  pexmidlem7N  30165  pl42lem2N  30169  pl42lem3N  30170  pl42lem4N  30171  pl42N  30172  lhprelat3N  30229  4atex  30265  lauteq  30284  lautco  30286  ltrncoidN  30317  ltrneq2  30337  ltrnideq  30364  trlnle  30375  trlval3  30376  cdlemc  30386  cdlemd9  30395  cdlemd  30396  cdleme21j  30525  cdleme21  30526  cdleme29ex  30563  cdlemefr27cl  30592  cdlemefs27cl  30602  cdleme32d  30633  cdleme32f  30635  cdleme35h2  30646  cdleme40m  30656  cdleme17d3  30685  cdleme48fvg  30689  cdlemeg46fvcl  30695  cdlemeg46fgN  30723  cdleme48fgv  30727  cdleme50trn3  30742  cdlemb3  30795  cdlemg8  30820  cdlemg11a  30826  cdlemg15a  30844  cdlemg15  30845  cdlemg16  30846  cdlemg16z  30848  cdlemg17dN  30852  cdlemg24  30877  cdlemg37  30878  cdlemg29  30894  cdlemg33b  30896  cdlemg38  30904  cdlemg40  30906  trlco  30916  cdlemg44b  30921  ltrncom  30927  trljco  30929  tendococl  30961  tendoplcl  30970  tendoplcom  30971  cdlemj2  31011  tendoid0  31014  tendo1ne0  31017  cdlemk25-3  31093  cdlemk36  31102  cdlemkid4  31123  cdlemk19x  31132  cdlemk53  31146  cdlemk56  31160  cdleml5N  31169  tendospcanN  31213  cdlemm10N  31308  dihord6apre  31446  dihord  31454  dihmeetlem1N  31480  dihglblem2N  31484  dihmeetlem2N  31489  dihmeetbN  31493  dihmeetlem5  31498  dihmeetlem6  31499  dihmeetlem7N  31500  dihmeetlem10N  31506  dihmeetlem12N  31508  dihmeetlem16N  31512  dihmeetlem17N  31513  dihmeetlem18N  31514  dihmeetALTN  31517  dihlspsnssN  31522  dvh3dim2  31638  dvh3dim3N  31639  lcfrlem16  31748  mapdrvallem2  31835  mapdh8ad  31969  hgmapvvlem3  32118
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator