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

Theorem simpl2 961
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 958 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 452 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simpll2  997  simprl2  1003  simp1l2  1051  simp2l2  1057  simp3l2  1063  3anandirs  1286  rspc3ev  3054  tfisi  4829  brcogw  5032  weniso  6066  smogt  6620  smorndom  6621  omeulem1  6816  nnmord  6866  nnmword  6867  difsnen  7181  mapunen  7267  ac6sfi  7342  ordiso2  7473  wemaplem2  7505  wemapso  7509  en2eqpr  7880  acndom  7921  infmap2  8087  cflim2  8132  cfsmolem  8139  coftr  8142  fin23lem26  8194  isf32lem9  8230  fin1a2lem9  8277  fin1a2lem10  8278  ac6num  8348  gchdomtri  8493  canth4  8511  gchpwdom  8538  gruima  8666  grudomon  8681  prn0  8855  distrlem4pr  8892  prlem934  8899  addcan  9239  addcan2  9240  ltmul1a  9848  ledivmulOLD  9873  supmul1  9962  uzsupss  10557  xaddass  10817  xleadd1a  10821  xlesubadd  10831  xmulass  10855  xlemul2a  10857  xadddilem  10862  xadddi  10863  ixxdisj  10920  ixxun  10921  ixxlb  10927  icoshftf1o  11009  icodisj  11011  lincmb01cmp  11027  iccf1o  11028  ltexp2a  11419  leexp2  11422  ltexp2r  11424  exple1  11427  expnlbnd2  11498  ccatass  11738  ccatopth  11764  s2f1o  11851  limsupgle  12259  limsupgre  12263  addcn2  12375  mulcn2  12377  dvdsval2  12843  dvdsadd2b  12880  dvdsmod  12894  oexpneg  12899  sadass  12971  gcdass  13033  rplpwr  13044  rppwr  13045  coprmdvds2  13091  rpmulgcd2  13093  rpexp  13108  rpdvds  13112  prmdiveq  13163  odzdvds  13169  coprimeprodsq2  13172  pythagtriplem3  13180  pythagtriplem4  13181  pcdvdsb  13230  vdwnnlem1  13351  0ram  13376  ramz2  13380  ramub1lem1  13382  mremre  13817  mrieqv2d  13852  lubss  14536  lubun  14538  clatleglb  14541  clatglbss  14542  mrelatglb  14598  issubmnd  14712  gsumccat  14775  frmdss2  14796  nmzsubg  14969  ghmnsgima  15017  odmodnn0  15166  odnncl  15171  odmod  15172  oddvds  15173  odeq  15176  odmulgid  15178  odmulgeq  15181  odbezout  15182  odf1o1  15194  odf1o2  15195  odngen  15199  gexdvdsi  15205  pgpfi1  15217  odcau  15226  subgslw  15238  fislw  15247  lsmless1x  15266  lsmless2x  15267  lsmsubm  15275  lsmmod  15295  lsmmod2  15296  efgsfo  15359  odadd1  15451  odadd2  15452  odadd  15453  lsmcomx  15459  prdscmnd  15464  gsumconst  15520  rng1eq0  15690  mulgass2  15698  cntzsubr  15888  isabvd  15896  0lmhm  16104  lmhmvsca  16109  reslmhm2b  16118  lbspss  16142  lspsnat  16205  lidldvgen  16314  issubassa  16371  coe1subfv  16647  coe1sclmul  16662  coe1sclmul2  16664  xrsdsreclblem  16732  cssmre  16908  obs2ss  16944  topssnei  17176  cnconst2  17335  cnpresti  17340  cnprest2  17342  cnpdis  17345  cnt0  17398  cnt1  17402  cnhaus  17406  sscmp  17456  hauscmp  17458  cnconn  17473  uncon  17480  kgen2ss  17575  ptpjopn  17632  prdstopn  17648  ptrescn  17659  qtopss  17735  kqfvima  17750  fbssint  17858  fbasrn  17904  filuni  17905  fmss  17966  rnelfm  17973  fmufil  17979  fmco  17981  flimss2  17992  flimss1  17993  flimrest  18003  cnpflf2  18020  flfcnp  18024  supnfcls  18040  fclsss1  18042  fclsss2  18043  isfcf  18054  subgntr  18124  opnsubg  18125  cldsubg  18128  ghmcnp  18132  ustuqtop1  18259  bldisj  18416  blgt0  18417  bl2in  18418  blss2ps  18421  blss2  18422  blssps  18442  blss  18443  xmetresbl  18455  lpbl  18521  blcld  18523  stdbdmopn  18536  metcnp3  18558  metcnp  18559  metcnp2  18560  txmetcnp  18565  blval2  18593  nmoix  18751  nmoi2  18752  nmotri  18761  metdsge  18867  metdseq0  18872  iocopnst  18953  xrhmeo  18959  nmhmcn  19116  cphsqrcl2  19137  cphsqrcl3  19138  pjth  19328  ovoliunlem2  19387  volun  19427  mbfimaopn2  19537  iblconst  19697  limcvallem  19746  dvfval  19772  dvcnp2  19794  dvcn  19795  evlsval2  19929  deg1mul3le  20027  deg1tmle  20028  dvdsq1p  20071  ig1peu  20082  ig1pdvds  20087  ply1term  20111  coeid3  20147  dgrmulc  20177  dvply1  20189  aaliou2  20245  efcvx  20353  tanord  20428  eflogeq  20484  logdivlti  20503  logccv  20542  recxpcl  20554  cxplea  20575  cxpeq  20629  ang180  20644  isosctrlem2  20651  cxp2lim  20803  amgm  20817  muval1  20904  dvdssqf  20909  mumullem2  20951  mumul  20952  bcmono  21049  lgsneg  21091  lgsdilem  21094  lgsdirprm  21101  lgsdir  21102  lgsdi  21104  lgsne0  21105  cyclispthon  21608  vdgrfval  21654  gxcom  21845  gxnn0add  21850  nvmul0or  22121  ipval2lem2  22188  ipval2lem5  22194  lnoadd  22247  lnosub  22248  lnomul  22249  shless  22849  shlej1  22850  kbmul  23446  homco2  23468  kbass2  23608  eliccelico  24128  elicoelioo  24129  iocinioc2  24130  iocinif  24132  difioo  24133  xrge0adddir  24203  xrge0npcan  24204  isarchi2  24243  rhmdvdsr  24244  pstmfval  24279  fmcncfil  24305  zrhnm  24341  qqhnm  24362  volfiniune  24574  dya2iocnrect  24619  probinc  24667  cndprob01  24681  cvmsss2  24949  cvmlift2lem10  24987  binomrisefac  25347  br6  25369  funsseq  25380  frrlem4  25539  brbtwn2  25792  colinearalglem1  25793  colinearalg  25797  axcgrtr  25802  axsegconlem8  25811  axsegconlem9  25812  axsegconlem10  25813  axcontlem2  25852  axcontlem10  25860  cgrtriv  25884  5segofs  25888  btwnouttr2  25904  btwnxfr  25938  lineext  25958  btwnconn1lem13  25981  brsegle2  25991  nn0prpwlem  26262  finlocfin  26316  comppfsc  26324  blbnd  26433  ismtyima  26449  rrndstprj2  26477  ghomdiv  26496  grpokerinj  26497  ofmpteq  26713  diophrw  26754  eldioph2lem1  26755  diophrex  26771  rencldnfi  26819  pellexlem2  26830  pellqrexplicit  26877  infmrgelbi  26878  pellfundglb  26885  pellfund14gap  26887  rmxycomplete  26917  congadd  26968  acongeq  26985  jm2.19  27001  jm2.23  27004  jm2.20nn  27005  jm2.27  27016  jm3.1  27028  lnmepi  27098  lmhmlnmsplit  27100  pwssplit1  27103  pwssplit2  27104  pwssplit3  27105  uvcresum  27157  frlmsslsp  27163  frlmup4  27168  enfixsn  27172  lindff1  27205  f1lindf  27207  lsslindf  27215  islindf4  27223  hbtlem2  27243  dgraa0p  27269  psgnunilem4  27335  idomrootle  27426  hashgcdlem  27431  proot1hash  27434  rfcnnnub  27621  climsuse  27648  stoweidlem17  27680  stoweidlem19  27682  stoweidlem20  27683  stoweidlem22  27685  stoweidlem28  27691  stoweidlem34  27697  stoweidlem44  27707  stoweidlem60  27723  wallispilem3  27730  modaddmulmod  28064  swrdnd  28074  swrdccatin12lem1  28094  swrdccatin12lem3a  28096  swrdccatin12lem4  28100  shwrdeqdif2lem1  28154  shwrdssizelem1a  28165  usgreghash2spot  28316  bnj517  29110  lubunNEW  29610  lsatfixedN  29646  lssat  29653  lshpkrlem4  29750  op0cl  29821  cvrcon3b  29914  atlen0  29947  atcvreq0  29951  atnle  29954  atlatmstc  29956  atlatle  29957  cvlcvr1  29976  hlsupr2  30023  hlrelat2  30039  cvrexchlem  30055  lnnat  30063  atcvrj2b  30068  3dimlem3  30097  3dim1  30103  1cvrjat  30111  llni  30144  llni2  30148  llnexatN  30157  2llnmat  30160  lplni  30168  2atnelpln  30180  llncvrlpln2  30193  2llnmj  30196  lplnexatN  30199  lplnexllnN  30200  2llnm3N  30205  lvoli  30211  lvoli3  30213  lvolnle3at  30218  islvol2aN  30228  4atlem4a  30235  4atlem4b  30236  4atlem11  30245  lplncvrlvol2  30251  2lplnmj  30258  islinei  30376  linepmap  30411  lnjatN  30416  lncvrat  30418  lncmp  30419  elpaddn0  30436  elpaddatriN  30439  elpaddat  30440  paddcom  30449  paddss2  30454  paddss12  30455  paddasslem4  30459  paddasslem9  30464  paddasslem10  30465  pmodl42N  30487  pmapjoin  30488  llnmod1i2  30496  polcon2bN  30556  pclfinclN  30586  poml4N  30589  poml6N  30591  osumcllem1N  30592  osumcllem2N  30593  osumcllem11N  30602  osumclN  30603  pmapojoinN  30604  pexmidlem2N  30607  pexmidlem3N  30608  pexmidlem4N  30609  pexmidlem6N  30611  pexmidlem7N  30612  pl42lem2N  30616  pl42lem3N  30617  pl42lem4N  30618  pl42N  30619  lhprelat3N  30676  4atex  30712  lauteq  30731  lautco  30733  ltrncoidN  30764  ltrneq2  30784  ltrnideq  30811  trlnle  30822  trlval3  30823  cdlemc  30833  cdlemd9  30842  cdlemd  30843  cdleme21j  30972  cdleme21  30973  cdleme29ex  31010  cdlemefr27cl  31039  cdlemefs27cl  31049  cdleme32d  31080  cdleme32f  31082  cdleme35h2  31093  cdleme40m  31103  cdleme17d3  31132  cdleme48fvg  31136  cdlemeg46fvcl  31142  cdlemeg46fgN  31170  cdleme48fgv  31174  cdleme50trn3  31189  cdlemb3  31242  cdlemg8  31267  cdlemg11a  31273  cdlemg15a  31291  cdlemg15  31292  cdlemg16  31293  cdlemg16z  31295  cdlemg17dN  31299  cdlemg24  31324  cdlemg37  31325  cdlemg29  31341  cdlemg33b  31343  cdlemg38  31351  cdlemg40  31353  trlco  31363  cdlemg44b  31368  ltrncom  31374  trljco  31376  tendococl  31408  tendoplcl  31417  tendoplcom  31418  cdlemj2  31458  tendoid0  31461  tendo1ne0  31464  cdlemk25-3  31540  cdlemk36  31549  cdlemkid4  31570  cdlemk19x  31579  cdlemk53  31593  cdlemk56  31607  cdleml5N  31616  tendospcanN  31660  cdlemm10N  31755  dihord6apre  31893  dihord  31901  dihmeetlem1N  31927  dihglblem2N  31931  dihmeetlem2N  31936  dihmeetbN  31940  dihmeetlem5  31945  dihmeetlem6  31946  dihmeetlem7N  31947  dihmeetlem10N  31953  dihmeetlem12N  31955  dihmeetlem16N  31959  dihmeetlem17N  31960  dihmeetlem18N  31961  dihmeetALTN  31964  dihlspsnssN  31969  dvh3dim2  32085  dvh3dim3N  32086  lcfrlem16  32195  mapdrvallem2  32282  mapdh8ad  32416  hgmapvvlem3  32565
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator