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

Theorem simpl2 1018
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 1015 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 471 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  simpll2  1054  simprl2  1060  simp1l2  1108  simp2l2  1114  simp3l2  1120  3anandirs  1382  rspc3ev  3175  brcogw  5022  f1prex  6207  weniso  6270  ofmpteq  6577  tfisi  6712  mpt2sn  6914  smogt  7112  smorndom  7113  omeulem1  7309  nnmord  7359  nnmword  7360  difsnen  7680  enfixsn  7707  mapunen  7767  ac6sfi  7841  ordiso2  8056  wemaplem2  8088  wemapso  8092  wemapso2lem  8093  en2eqpr  8464  acndom  8508  infmap2  8674  cflim2  8719  cfsmolem  8726  coftr  8729  fin23lem26  8781  isf32lem9  8817  fin1a2lem9  8864  fin1a2lem10  8865  ac6num  8935  gchdomtri  9080  canth4  9098  gchpwdom  9121  gruima  9253  grudomon  9268  prn0  9440  distrlem4pr  9477  prlem934  9484  addcan  9843  addcan2  9844  ltmul1a  10482  supmul1  10604  uzsupss  11285  xaddass  11564  xleadd1a  11568  xlesubadd  11578  xmulass  11602  xlemul2a  11604  xadddilem  11609  xadddi  11610  ixxdisj  11679  ixxun  11680  ixxlb  11686  ixxlbOLD  11687  icoshftf1o  11784  icodisj  11786  lincmb01cmp  11804  iccf1o  11805  ssfzoulel  12036  modaddmulmod  12188  ltexp2a  12356  leexp2  12359  ltexp2r  12361  exple1  12364  expnlbnd2  12435  ccatass  12768  ccatopth  12863  swrdccatin12lem2a  12878  repswccat  12925  2cshw  12949  repsco  12973  s2f1o  13047  limsupgle  13584  limsupgre  13591  limsupgreOLD  13592  addcn2  13706  mulcn2  13708  binomrisefac  14144  dvdsval2  14357  dvdsadd2b  14396  dvdsmod  14411  oexpneg  14417  sadass  14494  gcdass  14562  rplpwr  14573  rppwr  14574  lcmass  14628  coprmdvds2  14709  rpmulgcd2  14711  rpexp  14721  rpdvds  14725  coprmprod  14727  prmdiveq  14783  odzdvds  14789  odzdvdsOLD  14795  coprimeprodsq2  14809  pythagtriplem3  14817  pythagtriplem4  14818  pcdvdsb  14867  vdwnnlem1  14994  0ram  15027  ramz2  15031  ramub1lem1  15033  mremre  15559  mrieqv2d  15594  lubss  16416  lubun  16418  clatleglb  16421  clatglbss  16422  mrelatglb  16479  isnsgrp  16580  issubmnd  16613  gsumccat  16674  frmdss2  16696  nmzsubg  16907  ghmnsgima  16955  gsmsymgreqlem1  17120  psgnunilem4  17187  odmodnn0  17238  odnncl  17243  odmod  17244  oddvds  17245  odeq  17248  odmulgid  17254  odmulgeq  17257  odbezout  17258  odf1o1  17270  odf1o2  17271  odngen  17275  gexdvdsi  17283  pgpfi1  17296  odcau  17305  subgslw  17317  fislw  17326  lsmless1x  17345  lsmless2x  17346  lsmsubm  17354  lsmmod  17374  lsmmod2  17375  efgsfo  17438  odadd1  17535  odadd2  17536  odadd  17537  lsmcomx  17543  prdscmnd  17548  gsumconst  17616  srg1zr  17811  csrgbinom  17828  ring1eq0  17869  mulgass2  17878  cntzsubr  18089  isabvd  18097  0lmhm  18312  lmhmvsca  18317  reslmhm2b  18326  pwssplit1  18331  pwssplit2  18332  pwssplit3  18333  lbspss  18354  lspsnat  18417  lidldvgen  18528  issubassa  18597  evlsval2  18792  coe1subfv  18908  coe1sclmul  18924  coe1sclmul2  18926  xrsdsreclblem  19063  cssmre  19305  obs2ss  19341  uvcresum  19400  frlmsslsp  19403  frlmup4  19408  lindff1  19427  f1lindf  19429  lsslindf  19437  islindf4  19445  mpt2matmul  19520  mamutpos  19532  scmatscmide  19581  mavmulsolcl  19625  mulmarep1gsum2  19648  mdetdiaglem  19672  mdetdiag  19673  mdetunilem1  19686  mdetunilem3  19688  mdetunilem9  19694  maducoeval2  19714  madurid  19718  slesolinvbi  19755  cramerimplem1  19757  cramerlem1  19761  cramer  19765  cpmatel2  19786  m2cpm  19814  m2pmfzmap  19820  m2cpminvid2lem  19827  m2cpminvid2  19828  decpmatmul  19845  pmatcollpw1lem2  19848  pmatcollpw1  19849  pmatcollpw2lem  19850  pmatcollpwfi  19855  pm2mpcl  19870  mply1topmatcl  19878  mp2pm2mplem2  19880  mp2pm2mplem4  19882  mp2pm2mplem5  19883  mp2pm2mp  19884  pm2mpghmlem2  19885  pm2mpghmlem1  19886  chfacfisfcpmat  19928  topssnei  20189  cnconst2  20348  cnpresti  20353  cnprest2  20355  cnpdis  20358  cnt0  20411  cnt1  20415  cnhaus  20419  sscmp  20469  hauscmp  20471  cnconn  20486  uncon  20493  finlocfin  20584  comppfsc  20596  kgen2ss  20619  ptpjopn  20676  prdstopn  20692  ptrescn  20703  qtopss  20779  kqfvima  20794  fbssint  20902  fbasrn  20948  filuni  20949  fmss  21010  rnelfm  21017  fmufil  21023  fmco  21025  flimss2  21036  flimss1  21037  flimrest  21047  cnpflf2  21064  flfcnp  21068  supnfcls  21084  fclsss1  21086  fclsss2  21087  isfcf  21098  subgntr  21170  opnsubg  21171  cldsubg  21174  ghmcnp  21178  ustuqtop1  21305  bldisj  21462  blgt0  21463  bl2in  21464  blss2ps  21467  blss2  21468  blssps  21488  blss  21489  xmetresbl  21501  lpbl  21567  blcld  21569  stdbdmopn  21582  metcnp3  21604  metcnp  21605  metcnp2  21606  txmetcnp  21611  blval2  21626  nmoix  21783  nmoi2  21784  nmoixOLD  21799  nmoi2OLD  21800  nmotri  21809  metdsge  21915  metdseq0  21920  metdsgeOLD  21930  metdseq0OLD  21935  iocopnst  22017  xrhmeo  22023  nmhmcn  22183  cphsqrtcl2  22213  cphsqrtcl3  22214  pjth  22442  ovoliunlem2  22505  volun  22547  mbfimaopn2  22662  iblconst  22824  limcvallem  22875  dvfval  22901  dvcnp2  22923  dvcn  22924  deg1mul3le  23114  deg1tmle  23115  dvdsq1p  23160  ig1peu  23171  ig1peuOLD  23172  ig1pdvds  23177  ig1pdvdsOLD  23183  ply1term  23207  coeid3  23243  dgrmulc  23274  dvply1  23286  aaliou2  23345  efcvx  23453  tanord  23536  eflogeq  23600  logdivlti  23618  logccv  23657  recxpcl  23669  cxplea  23690  cxpeq  23746  ang180  23792  isosctrlem2  23797  cxp2lim  23951  amgm  23965  muval1  24109  dvdssqf  24114  mumullem2  24156  mumul  24157  bcmono  24254  lgsneg  24296  lgsdilem  24299  lgsdirprm  24306  lgsdir  24307  lgsdi  24309  lgsne0  24310  brbtwn2  24984  colinearalglem1  24985  colinearalg  24989  axcgrtr  24994  axsegconlem8  25003  axsegconlem9  25004  axsegconlem10  25005  axcontlem2  25044  axcontlem10  25052  cyclispthon  25410  wwlknext  25501  clwlkisclwwlklem0  25565  erclwwlksym  25591  eleclclwwlknlem2  25595  erclwwlkneqlen  25601  erclwwlknsym  25603  vdgrfval  25672  nbhashuvtx1  25692  usgreghash2spot  25846  extwwlkfablem2  25855  numclwwlk3lem  25885  frgraregord13  25896  gxcom  26046  gxnn0add  26051  nvmul0or  26322  ipval2lem2  26389  ipval2lem5  26395  lnoadd  26448  lnosub  26449  lnomul  26450  shless  27061  shlej1  27062  kbmul  27657  homco2  27679  kbass2  27819  eliccelico  28408  elicoelioo  28409  iocinioc2  28410  iocinif  28412  difioo  28413  xrge0adddir  28504  xrge0npcan  28506  isarchi2  28551  archiabl  28564  rhmdvdsr  28630  pstmfval  28748  fmcncfil  28786  zrhnm  28822  qqhnm  28843  nexple  28880  volfiniune  29102  dya2iocnrect  29152  probinc  29303  cndprob01  29317  signswmnd  29495  bnj517  29745  cvmsss2  30046  cvmlift2lem10  30084  br6  30446  funsseq  30458  frrlem4  30566  cgrtriv  30818  5segofs  30822  btwnouttr2  30838  btwnxfr  30872  lineext  30892  btwnconn1lem13  30915  brsegle2  30925  nn0prpwlem  31027  blbnd  32164  ismtyima  32180  rrndstprj2  32208  ghomdiv  32227  grpokerinj  32228  lsatfixedN  32620  lssat  32627  lshpkrlem4  32724  cvrcon3b  32888  atlen0  32921  atcvreq0  32925  atnle  32928  atlatmstc  32930  atlatle  32931  cvlcvr1  32950  hlsupr2  32997  hlrelat2  33013  cvrexchlem  33029  lnnat  33037  atcvrj2b  33042  3dimlem3  33071  3dim1  33077  1cvrjat  33085  llni  33118  llni2  33122  llnexatN  33131  2llnmat  33134  lplni  33142  2atnelpln  33154  llncvrlpln2  33167  2llnmj  33170  lplnexatN  33173  lplnexllnN  33174  2llnm3N  33179  lvoli  33185  lvoli3  33187  lvolnle3at  33192  islvol2aN  33202  4atlem4a  33209  4atlem4b  33210  4atlem11  33219  lplncvrlvol2  33225  2lplnmj  33232  islinei  33350  linepmap  33385  lnjatN  33390  lncvrat  33392  lncmp  33393  elpaddn0  33410  elpaddatriN  33413  elpaddat  33414  paddcom  33423  paddss2  33428  paddss12  33429  paddasslem4  33433  paddasslem9  33438  paddasslem10  33439  pmodl42N  33461  pmapjoin  33462  llnmod1i2  33470  polcon2bN  33530  pclfinclN  33560  poml4N  33563  poml6N  33565  osumcllem1N  33566  osumcllem2N  33567  osumcllem11N  33576  osumclN  33577  pmapojoinN  33578  pexmidlem2N  33581  pexmidlem3N  33582  pexmidlem4N  33583  pexmidlem6N  33585  pexmidlem7N  33586  pl42lem2N  33590  pl42lem3N  33591  pl42lem4N  33592  pl42N  33593  lhprelat3N  33650  4atex  33686  lauteq  33705  lautco  33707  ltrncoidN  33738  ltrneq2  33758  ltrnideq  33786  trlnle  33797  trlval3  33798  cdlemc  33808  cdlemd9  33817  cdlemd  33818  cdleme21j  33948  cdleme21  33949  cdleme29ex  33986  cdlemefr27cl  34015  cdlemefs27cl  34025  cdleme32d  34056  cdleme32f  34058  cdleme35h2  34069  cdleme40m  34079  cdleme17d3  34108  cdleme48fvg  34112  cdlemeg46fvcl  34118  cdlemeg46fgN  34146  cdleme48fgv  34150  cdleme50trn3  34165  cdlemb3  34218  cdlemg8  34243  cdlemg11a  34249  cdlemg15a  34267  cdlemg15  34268  cdlemg16  34269  cdlemg16z  34271  cdlemg17dN  34275  cdlemg24  34300  cdlemg37  34301  cdlemg29  34317  cdlemg33b  34319  cdlemg38  34327  cdlemg40  34329  trlco  34339  cdlemg44b  34344  ltrncom  34350  trljco  34352  tendococl  34384  tendoplcl  34393  tendoplcom  34394  cdlemj2  34434  tendoid0  34437  tendo1ne0  34440  cdlemk25-3  34516  cdlemk36  34525  cdlemkid4  34546  cdlemk19x  34555  cdlemk53  34569  cdlemk56  34583  cdleml5N  34592  tendospcanN  34636  cdlemm10N  34731  dihord6apre  34869  dihord  34877  dihmeetlem1N  34903  dihglblem2N  34907  dihmeetlem2N  34912  dihmeetbN  34916  dihmeetlem5  34921  dihmeetlem6  34922  dihmeetlem7N  34923  dihmeetlem10N  34929  dihmeetlem12N  34931  dihmeetlem16N  34935  dihmeetlem17N  34936  dihmeetlem18N  34937  dihmeetALTN  34940  dihlspsnssN  34945  dvh3dim2  35061  dvh3dim3N  35062  lcfrlem16  35171  mapdrvallem2  35258  mapdh8ad  35392  hgmapvvlem3  35541  diophrw  35646  eldioph2lem1  35647  diophrex  35663  rencldnfi  35709  pellexlem2  35719  pellqrexplicit  35768  infmrgelbi  35769  infmrgelbiOLD  35770  pellfundglb  35778  pellfund14gap  35780  rmxycomplete  35810  congadd  35861  acongeq  35878  jm2.19  35893  jm2.23  35896  jm2.20nn  35897  jm2.27  35908  jm3.1  35920  lnmepi  35988  lmhmlnmsplit  35990  hbtlem2  36028  dgraa0p  36060  idomrootle  36114  hashgcdlem  36119  proot1hash  36122  iocunico  36140  iocinico  36141  relexpxpmin  36354  rfcnnnub  37397  uzwo4  37430  supxrge  37599  snunioo2  37644  iccintsng  37662  climsuse  37725  lptre2pt  37758  limcleqr  37763  0ellimcdiv  37768  dvnprodlem1  37859  volioc  37887  stoweidlem17  37915  stoweidlem19  37917  stoweidlem20  37918  stoweidlem22  37920  stoweidlem28  37926  stoweidlem34  37933  stoweidlem44  37943  stoweidlem60  37959  wallispilem3  37967  fourierdlem42  38050  fourierdlem42OLD  38051  fourierdlem48  38056  fourierdlem51  38059  fourierdlem54  38062  fourierdlem74  38082  fourierdlem77  38085  fourierdlem87  38095  fourierdlem97  38105  ovnsubaddlem2  38431  fzopredsuc  38758  oexpnegALTV  38844  oexpnegnz  38845  tgblthelfgott  38946  repswpfx  39017  fun2dmnop  39069  eluzge0nn0  39095  fzoopth  39105  ewlkle  39672  edginwlk  39695  rmsupp0  40426  rmsuppss  40428  lincresunit3lem3  40540  lincresunit3lem2  40546  lindssnlvec  40552  fdivmptf  40625  refdivmptf  40626  elbigolo1  40641
  Copyright terms: Public domain W3C validator