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  2907  tfisi  4665  weniso  5868  smogt  6400  smorndom  6401  omeulem1  6596  nnmord  6646  nnmword  6647  difsnen  6960  mapunen  7046  ac6sfi  7117  ordiso2  7246  wemaplem2  7278  wemapso  7282  en2eqpr  7653  acndom  7694  infmap2  7860  cflim2  7905  cfsmolem  7912  coftr  7915  fin23lem26  7967  isf32lem9  8003  fin1a2lem9  8050  fin1a2lem10  8051  ac6num  8122  gchdomtri  8267  canth4  8285  gchpwdom  8312  gruima  8440  grudomon  8455  prn0  8629  distrlem4pr  8666  prlem934  8673  addcan  9012  addcan2  9013  ltmul1a  9621  ledivmulOLD  9646  supmul1  9735  uzsupss  10326  xaddass  10585  xleadd1a  10589  xlesubadd  10599  xmulass  10623  xlemul2a  10625  xadddilem  10630  xadddi  10631  ixxdisj  10687  ixxun  10688  ixxlb  10694  icoshftf1o  10775  icodisj  10777  lincmb01cmp  10793  iccf1o  10794  ltexp2a  11169  leexp2  11172  ltexp2r  11174  exple1  11177  expnlbnd2  11248  ccatass  11452  ccatopth  11478  limsupgle  11967  limsupgre  11971  addcn2  12083  mulcn2  12085  dvdsval2  12550  dvdsadd2b  12587  dvdsmod  12601  oexpneg  12606  sadass  12678  gcdass  12740  rplpwr  12751  rppwr  12752  coprmdvds2  12798  rpmulgcd2  12800  rpexp  12815  rpdvds  12819  prmdiveq  12870  odzdvds  12876  coprimeprodsq2  12879  pythagtriplem3  12887  pythagtriplem4  12888  pcdvdsb  12937  vdwnnlem1  13058  0ram  13083  ramz2  13087  ramub1lem1  13089  mremre  13522  mrieqv2d  13557  lubss  14241  lubun  14243  clatleglb  14246  clatglbss  14247  mrelatglb  14303  issubmnd  14417  gsumccat  14480  frmdss2  14501  nmzsubg  14674  ghmnsgima  14722  odmodnn0  14871  odnncl  14876  odmod  14877  oddvds  14878  odeq  14881  odmulgid  14883  odmulgeq  14886  odbezout  14887  odf1o1  14899  odf1o2  14900  odngen  14904  gexdvdsi  14910  pgpfi1  14922  odcau  14931  subgslw  14943  fislw  14952  lsmless1x  14971  lsmless2x  14972  lsmsubm  14980  lsmmod  15000  lsmmod2  15001  efgsfo  15064  odadd1  15156  odadd2  15157  odadd  15158  lsmcomx  15164  prdscmnd  15169  gsumconst  15225  rng1eq0  15395  mulgass2  15403  cntzsubr  15593  isabvd  15601  0lmhm  15813  lmhmvsca  15818  reslmhm2b  15827  lbspss  15851  lspsnat  15914  lidldvgen  16023  issubassa  16080  coe1subfv  16359  coe1sclmul  16374  coe1sclmul2  16376  xrsdsreclblem  16433  cssmre  16609  obs2ss  16645  topssnei  16877  cnconst2  17027  cnpresti  17032  cnprest2  17034  cnpdis  17037  cnt0  17090  cnt1  17094  cnhaus  17098  sscmp  17148  hauscmp  17150  cnconn  17164  uncon  17171  kgen2ss  17266  ptpjopn  17322  prdstopn  17338  ptrescn  17349  qtopss  17422  kqfvima  17437  fbssint  17549  fbasrn  17595  filuni  17596  fmss  17657  rnelfm  17664  fmufil  17670  fmco  17672  flimss2  17683  flimss1  17684  flimrest  17694  cnpflf2  17711  flfcnp  17715  supnfcls  17731  fclsss1  17733  fclsss2  17734  isfcf  17745  subgntr  17805  opnsubg  17806  cldsubg  17809  ghmcnp  17813  bldisj  17971  blgt0  17972  bl2in  17973  blss2  17975  blss  17988  xmetresbl  17999  lpbl  18065  blcld  18067  stdbdmopn  18080  metcnp3  18102  metcnp  18103  metcnp2  18104  txmetcnp  18109  nmoix  18254  nmoi2  18255  nmotri  18264  metdsge  18369  metdseq0  18374  iocopnst  18454  xrhmeo  18460  nmhmcn  18617  cphsqrcl2  18638  cphsqrcl3  18639  pjth  18819  ovoliunlem2  18878  volun  18918  mbfimaopn2  19028  iblconst  19188  limcvallem  19237  dvfval  19263  dvcnp2  19285  dvcn  19286  evlsval2  19420  deg1mul3le  19518  deg1tmle  19519  dvdsq1p  19562  ig1peu  19573  ig1pdvds  19578  ply1term  19602  coeid3  19638  dgrmulc  19668  dvply1  19680  aaliou2  19736  efcvx  19841  tanord  19916  eflogeq  19971  logdivlti  19987  logccv  20026  recxpcl  20038  cxplea  20059  cxpeq  20113  ang180  20128  isosctrlem2  20135  cxp2lim  20287  amgm  20301  muval1  20387  dvdssqf  20392  mumullem2  20434  mumul  20435  bcmono  20532  lgsneg  20574  lgsdilem  20577  lgsdirprm  20584  lgsdir  20585  lgsdi  20587  lgsne0  20588  gxcom  20952  gxnn0add  20957  nvmul0or  21226  ipval2lem2  21293  ipval2lem5  21299  lnoadd  21352  lnosub  21353  lnomul  21354  shless  21954  shlej1  21955  kbmul  22551  homco2  22573  kbass2  22713  eliccelico  23285  elicoelioo  23286  iocinioc2  23287  iocinif  23289  difioo  23290  xrge0adddir  23347  xrge0npcan  23348  probinc  23639  cndprob01  23653  cvmsss2  23820  cvmlift2lem10  23858  vdgrfval  23904  faclimlem5  24121  br6  24185  funsseq  24196  frrlem4  24355  brbtwn2  24605  colinearalglem1  24606  colinearalg  24610  axcgrtr  24615  axsegconlem8  24624  axsegconlem9  24625  axsegconlem10  24626  axcontlem2  24665  axcontlem10  24673  cgrtriv  24697  5segofs  24701  btwnouttr2  24717  btwnxfr  24751  lineext  24771  btwnconn1lem13  24794  brsegle2  24804  sndw  25203  mapmapmap  25251  iscst4  25280  cmprtr  25499  rltrran  25517  rltrooo  25518  cnrsfin  25628  cnrscoa  25629  efilcp  25655  fgsb2  25658  cmptdst  25671  cmptdst2  25674  limptlimpr2lem2  25678  flfnei2  25680  islimrs3  25684  usinuniopb  25697  lvsovso  25729  addcanri  25769  negveud  25771  mulmulvec  25790  distmlva  25791  distsava  25792  isder  25810  iepiclem  25926  tartarmap  25991  indcls2  26099  lppotos  26247  pdiveql  26271  nn0prpwlem  26341  finlocfin  26402  comppfsc  26410  blbnd  26614  ismtyima  26630  rrndstprj2  26658  ghomdiv  26677  grpokerinj  26678  ofmpteq  26900  diophrw  26941  eldioph2lem1  26942  diophrex  26958  rencldnfi  27007  pellexlem2  27018  pellqrexplicit  27065  infmrgelbi  27066  pellfundglb  27073  pellfund14gap  27075  rmxycomplete  27105  congadd  27156  acongeq  27173  jm2.19  27189  jm2.23  27192  jm2.20nn  27193  jm2.27  27204  jm3.1  27216  lnmepi  27286  lmhmlnmsplit  27288  pwssplit1  27291  pwssplit2  27292  pwssplit3  27293  uvcresum  27345  frlmsslsp  27351  frlmup4  27356  enfixsn  27360  lindff1  27393  f1lindf  27395  lsslindf  27403  islindf4  27411  hbtlem2  27431  dgraa0p  27457  psgnunilem4  27523  idomrootle  27614  hashgcdlem  27619  proot1hash  27622  rfcnnnub  27810  climsuse  27837  stoweidlem19  27871  stoweidlem20  27872  stoweidlem22  27874  stoweidlem28  27880  stoweidlem34  27886  stoweidlem44  27896  stoweidlem51  27903  stoweidlem60  27912  wallispilem3  27919  s2f1o  28223  cyclispthon  28378  bnj517  29233  lubunNEW  29785  lsatfixedN  29821  lssat  29828  lshpkrlem4  29925  op0cl  29996  cvrcon3b  30089  atlen0  30122  atcvreq0  30126  atnle  30129  atlatmstc  30131  atlatle  30132  cvlcvr1  30151  hlsupr2  30198  hlrelat2  30214  cvrexchlem  30230  lnnat  30238  atcvrj2b  30243  3dimlem3  30272  3dim1  30278  1cvrjat  30286  llni  30319  llni2  30323  llnexatN  30332  2llnmat  30335  lplni  30343  2atnelpln  30355  llncvrlpln2  30368  2llnmj  30371  lplnexatN  30374  lplnexllnN  30375  2llnm3N  30380  lvoli  30386  lvoli3  30388  lvolnle3at  30393  islvol2aN  30403  4atlem4a  30410  4atlem4b  30411  4atlem11  30420  lplncvrlvol2  30426  2lplnmj  30433  islinei  30551  linepmap  30586  lnjatN  30591  lncvrat  30593  lncmp  30594  elpaddn0  30611  elpaddatriN  30614  elpaddat  30615  paddcom  30624  paddss2  30629  paddss12  30630  paddasslem4  30634  paddasslem9  30639  paddasslem10  30640  pmodl42N  30662  pmapjoin  30663  llnmod1i2  30671  polcon2bN  30731  pclfinclN  30761  poml4N  30764  poml6N  30766  osumcllem1N  30767  osumcllem2N  30768  osumcllem11N  30777  osumclN  30778  pmapojoinN  30779  pexmidlem2N  30782  pexmidlem3N  30783  pexmidlem4N  30784  pexmidlem6N  30786  pexmidlem7N  30787  pl42lem2N  30791  pl42lem3N  30792  pl42lem4N  30793  pl42N  30794  lhprelat3N  30851  4atex  30887  lauteq  30906  lautco  30908  ltrncoidN  30939  ltrneq2  30959  ltrnideq  30986  trlnle  30997  trlval3  30998  cdlemc  31008  cdlemd9  31017  cdlemd  31018  cdleme21j  31147  cdleme21  31148  cdleme29ex  31185  cdlemefr27cl  31214  cdlemefs27cl  31224  cdleme32d  31255  cdleme32f  31257  cdleme35h2  31268  cdleme40m  31278  cdleme17d3  31307  cdleme48fvg  31311  cdlemeg46fvcl  31317  cdlemeg46fgN  31345  cdleme48fgv  31349  cdleme50trn3  31364  cdlemb3  31417  cdlemg8  31442  cdlemg11a  31448  cdlemg15a  31466  cdlemg15  31467  cdlemg16  31468  cdlemg16z  31470  cdlemg17dN  31474  cdlemg24  31499  cdlemg37  31500  cdlemg29  31516  cdlemg33b  31518  cdlemg38  31526  cdlemg40  31528  trlco  31538  cdlemg44b  31543  ltrncom  31549  trljco  31551  tendococl  31583  tendoplcl  31592  tendoplcom  31593  cdlemj2  31633  tendoid0  31636  tendo1ne0  31639  cdlemk25-3  31715  cdlemk36  31724  cdlemkid4  31745  cdlemk19x  31754  cdlemk53  31768  cdlemk56  31782  cdleml5N  31791  tendospcanN  31835  cdlemm10N  31930  dihord6apre  32068  dihord  32076  dihmeetlem1N  32102  dihglblem2N  32106  dihmeetlem2N  32111  dihmeetbN  32115  dihmeetlem5  32120  dihmeetlem6  32121  dihmeetlem7N  32122  dihmeetlem10N  32128  dihmeetlem12N  32130  dihmeetlem16N  32134  dihmeetlem17N  32135  dihmeetlem18N  32136  dihmeetALTN  32139  dihlspsnssN  32144  dvh3dim2  32260  dvh3dim3N  32261  lcfrlem16  32370  mapdrvallem2  32457  mapdh8ad  32591  hgmapvvlem3  32740
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