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  3022  tfisi  4797  brcogw  5000  weniso  6034  smogt  6588  smorndom  6589  omeulem1  6784  nnmord  6834  nnmword  6835  difsnen  7149  mapunen  7235  ac6sfi  7310  ordiso2  7440  wemaplem2  7472  wemapso  7476  en2eqpr  7847  acndom  7888  infmap2  8054  cflim2  8099  cfsmolem  8106  coftr  8109  fin23lem26  8161  isf32lem9  8197  fin1a2lem9  8244  fin1a2lem10  8245  ac6num  8315  gchdomtri  8460  canth4  8478  gchpwdom  8505  gruima  8633  grudomon  8648  prn0  8822  distrlem4pr  8859  prlem934  8866  addcan  9206  addcan2  9207  ltmul1a  9815  ledivmulOLD  9840  supmul1  9929  uzsupss  10524  xaddass  10784  xleadd1a  10788  xlesubadd  10798  xmulass  10822  xlemul2a  10824  xadddilem  10829  xadddi  10830  ixxdisj  10887  ixxun  10888  ixxlb  10894  icoshftf1o  10976  icodisj  10978  lincmb01cmp  10994  iccf1o  10995  ltexp2a  11386  leexp2  11389  ltexp2r  11391  exple1  11394  expnlbnd2  11465  ccatass  11705  ccatopth  11731  s2f1o  11818  limsupgle  12226  limsupgre  12230  addcn2  12342  mulcn2  12344  dvdsval2  12810  dvdsadd2b  12847  dvdsmod  12861  oexpneg  12866  sadass  12938  gcdass  13000  rplpwr  13011  rppwr  13012  coprmdvds2  13058  rpmulgcd2  13060  rpexp  13075  rpdvds  13079  prmdiveq  13130  odzdvds  13136  coprimeprodsq2  13139  pythagtriplem3  13147  pythagtriplem4  13148  pcdvdsb  13197  vdwnnlem1  13318  0ram  13343  ramz2  13347  ramub1lem1  13349  mremre  13784  mrieqv2d  13819  lubss  14503  lubun  14505  clatleglb  14508  clatglbss  14509  mrelatglb  14565  issubmnd  14679  gsumccat  14742  frmdss2  14763  nmzsubg  14936  ghmnsgima  14984  odmodnn0  15133  odnncl  15138  odmod  15139  oddvds  15140  odeq  15143  odmulgid  15145  odmulgeq  15148  odbezout  15149  odf1o1  15161  odf1o2  15162  odngen  15166  gexdvdsi  15172  pgpfi1  15184  odcau  15193  subgslw  15205  fislw  15214  lsmless1x  15233  lsmless2x  15234  lsmsubm  15242  lsmmod  15262  lsmmod2  15263  efgsfo  15326  odadd1  15418  odadd2  15419  odadd  15420  lsmcomx  15426  prdscmnd  15431  gsumconst  15487  rng1eq0  15657  mulgass2  15665  cntzsubr  15855  isabvd  15863  0lmhm  16071  lmhmvsca  16076  reslmhm2b  16085  lbspss  16109  lspsnat  16172  lidldvgen  16281  issubassa  16338  coe1subfv  16614  coe1sclmul  16629  coe1sclmul2  16631  xrsdsreclblem  16699  cssmre  16875  obs2ss  16911  topssnei  17143  cnconst2  17301  cnpresti  17306  cnprest2  17308  cnpdis  17311  cnt0  17364  cnt1  17368  cnhaus  17372  sscmp  17422  hauscmp  17424  cnconn  17438  uncon  17445  kgen2ss  17540  ptpjopn  17597  prdstopn  17613  ptrescn  17624  qtopss  17700  kqfvima  17715  fbssint  17823  fbasrn  17869  filuni  17870  fmss  17931  rnelfm  17938  fmufil  17944  fmco  17946  flimss2  17957  flimss1  17958  flimrest  17968  cnpflf2  17985  flfcnp  17989  supnfcls  18005  fclsss1  18007  fclsss2  18008  isfcf  18019  subgntr  18089  opnsubg  18090  cldsubg  18093  ghmcnp  18097  ustuqtop1  18224  bldisj  18381  blgt0  18382  bl2in  18383  blss2ps  18386  blss2  18387  blssps  18407  blss  18408  xmetresbl  18420  lpbl  18486  blcld  18488  stdbdmopn  18501  metcnp3  18523  metcnp  18524  metcnp2  18525  txmetcnp  18530  blval2  18558  nmoix  18716  nmoi2  18717  nmotri  18726  metdsge  18832  metdseq0  18837  iocopnst  18918  xrhmeo  18924  nmhmcn  19081  cphsqrcl2  19102  cphsqrcl3  19103  pjth  19293  ovoliunlem2  19352  volun  19392  mbfimaopn2  19502  iblconst  19662  limcvallem  19711  dvfval  19737  dvcnp2  19759  dvcn  19760  evlsval2  19894  deg1mul3le  19992  deg1tmle  19993  dvdsq1p  20036  ig1peu  20047  ig1pdvds  20052  ply1term  20076  coeid3  20112  dgrmulc  20142  dvply1  20154  aaliou2  20210  efcvx  20318  tanord  20393  eflogeq  20449  logdivlti  20468  logccv  20507  recxpcl  20519  cxplea  20540  cxpeq  20594  ang180  20609  isosctrlem2  20616  cxp2lim  20768  amgm  20782  muval1  20869  dvdssqf  20874  mumullem2  20916  mumul  20917  bcmono  21014  lgsneg  21056  lgsdilem  21059  lgsdirprm  21066  lgsdir  21067  lgsdi  21069  lgsne0  21070  cyclispthon  21573  vdgrfval  21619  gxcom  21810  gxnn0add  21815  nvmul0or  22086  ipval2lem2  22153  ipval2lem5  22159  lnoadd  22212  lnosub  22213  lnomul  22214  shless  22814  shlej1  22815  kbmul  23411  homco2  23433  kbass2  23573  eliccelico  24093  elicoelioo  24094  iocinioc2  24095  iocinif  24097  difioo  24098  xrge0adddir  24168  xrge0npcan  24169  isarchi2  24208  rhmdvdsr  24209  pstmfval  24244  fmcncfil  24270  zrhnm  24306  qqhnm  24327  volfiniune  24539  dya2iocnrect  24584  probinc  24632  cndprob01  24646  cvmsss2  24914  cvmlift2lem10  24952  binomrisefac  25309  br6  25328  funsseq  25339  frrlem4  25498  brbtwn2  25748  colinearalglem1  25749  colinearalg  25753  axcgrtr  25758  axsegconlem8  25767  axsegconlem9  25768  axsegconlem10  25769  axcontlem2  25808  axcontlem10  25816  cgrtriv  25840  5segofs  25844  btwnouttr2  25860  btwnxfr  25894  lineext  25914  btwnconn1lem13  25937  brsegle2  25947  nn0prpwlem  26215  finlocfin  26269  comppfsc  26277  blbnd  26386  ismtyima  26402  rrndstprj2  26430  ghomdiv  26449  grpokerinj  26450  ofmpteq  26666  diophrw  26707  eldioph2lem1  26708  diophrex  26724  rencldnfi  26772  pellexlem2  26783  pellqrexplicit  26830  infmrgelbi  26831  pellfundglb  26838  pellfund14gap  26840  rmxycomplete  26870  congadd  26921  acongeq  26938  jm2.19  26954  jm2.23  26957  jm2.20nn  26958  jm2.27  26969  jm3.1  26981  lnmepi  27051  lmhmlnmsplit  27053  pwssplit1  27056  pwssplit2  27057  pwssplit3  27058  uvcresum  27110  frlmsslsp  27116  frlmup4  27121  enfixsn  27125  lindff1  27158  f1lindf  27160  lsslindf  27168  islindf4  27176  hbtlem2  27196  dgraa0p  27222  psgnunilem4  27288  idomrootle  27379  hashgcdlem  27384  proot1hash  27387  rfcnnnub  27574  climsuse  27601  stoweidlem17  27633  stoweidlem19  27635  stoweidlem20  27636  stoweidlem22  27638  stoweidlem28  27644  stoweidlem34  27650  stoweidlem44  27660  stoweidlem60  27676  wallispilem3  27683  swrdnd  28001  swrdccatin12lem1  28019  swrdccatin12lem3a  28021  swrdccatin12lem4  28025  usgreghash2spot  28172  bnj517  28962  lubunNEW  29456  lsatfixedN  29492  lssat  29499  lshpkrlem4  29596  op0cl  29667  cvrcon3b  29760  atlen0  29793  atcvreq0  29797  atnle  29800  atlatmstc  29802  atlatle  29803  cvlcvr1  29822  hlsupr2  29869  hlrelat2  29885  cvrexchlem  29901  lnnat  29909  atcvrj2b  29914  3dimlem3  29943  3dim1  29949  1cvrjat  29957  llni  29990  llni2  29994  llnexatN  30003  2llnmat  30006  lplni  30014  2atnelpln  30026  llncvrlpln2  30039  2llnmj  30042  lplnexatN  30045  lplnexllnN  30046  2llnm3N  30051  lvoli  30057  lvoli3  30059  lvolnle3at  30064  islvol2aN  30074  4atlem4a  30081  4atlem4b  30082  4atlem11  30091  lplncvrlvol2  30097  2lplnmj  30104  islinei  30222  linepmap  30257  lnjatN  30262  lncvrat  30264  lncmp  30265  elpaddn0  30282  elpaddatriN  30285  elpaddat  30286  paddcom  30295  paddss2  30300  paddss12  30301  paddasslem4  30305  paddasslem9  30310  paddasslem10  30311  pmodl42N  30333  pmapjoin  30334  llnmod1i2  30342  polcon2bN  30402  pclfinclN  30432  poml4N  30435  poml6N  30437  osumcllem1N  30438  osumcllem2N  30439  osumcllem11N  30448  osumclN  30449  pmapojoinN  30450  pexmidlem2N  30453  pexmidlem3N  30454  pexmidlem4N  30455  pexmidlem6N  30457  pexmidlem7N  30458  pl42lem2N  30462  pl42lem3N  30463  pl42lem4N  30464  pl42N  30465  lhprelat3N  30522  4atex  30558  lauteq  30577  lautco  30579  ltrncoidN  30610  ltrneq2  30630  ltrnideq  30657  trlnle  30668  trlval3  30669  cdlemc  30679  cdlemd9  30688  cdlemd  30689  cdleme21j  30818  cdleme21  30819  cdleme29ex  30856  cdlemefr27cl  30885  cdlemefs27cl  30895  cdleme32d  30926  cdleme32f  30928  cdleme35h2  30939  cdleme40m  30949  cdleme17d3  30978  cdleme48fvg  30982  cdlemeg46fvcl  30988  cdlemeg46fgN  31016  cdleme48fgv  31020  cdleme50trn3  31035  cdlemb3  31088  cdlemg8  31113  cdlemg11a  31119  cdlemg15a  31137  cdlemg15  31138  cdlemg16  31139  cdlemg16z  31141  cdlemg17dN  31145  cdlemg24  31170  cdlemg37  31171  cdlemg29  31187  cdlemg33b  31189  cdlemg38  31197  cdlemg40  31199  trlco  31209  cdlemg44b  31214  ltrncom  31220  trljco  31222  tendococl  31254  tendoplcl  31263  tendoplcom  31264  cdlemj2  31304  tendoid0  31307  tendo1ne0  31310  cdlemk25-3  31386  cdlemk36  31395  cdlemkid4  31416  cdlemk19x  31425  cdlemk53  31439  cdlemk56  31453  cdleml5N  31462  tendospcanN  31506  cdlemm10N  31601  dihord6apre  31739  dihord  31747  dihmeetlem1N  31773  dihglblem2N  31777  dihmeetlem2N  31782  dihmeetbN  31786  dihmeetlem5  31791  dihmeetlem6  31792  dihmeetlem7N  31793  dihmeetlem10N  31799  dihmeetlem12N  31801  dihmeetlem16N  31805  dihmeetlem17N  31806  dihmeetlem18N  31807  dihmeetALTN  31810  dihlspsnssN  31815  dvh3dim2  31931  dvh3dim3N  31932  lcfrlem16  32041  mapdrvallem2  32128  mapdh8ad  32262  hgmapvvlem3  32411
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