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

Theorem simpl2 1009
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 1006 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 466 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simpll2  1045  simprl2  1051  simp1l2  1099  simp2l2  1105  simp3l2  1111  3anandirs  1367  rspc3ev  3201  brcogw  5023  f1prex  6197  weniso  6260  ofmpteq  6564  tfisi  6699  mpt2sn  6898  smogt  7094  smorndom  7095  omeulem1  7291  nnmord  7341  nnmword  7342  difsnen  7660  enfixsn  7687  mapunen  7747  ac6sfi  7821  ordiso2  8030  wemaplem2  8062  wemapso  8066  wemapso2lem  8067  en2eqpr  8437  acndom  8480  infmap2  8646  cflim2  8691  cfsmolem  8698  coftr  8701  fin23lem26  8753  isf32lem9  8789  fin1a2lem9  8836  fin1a2lem10  8837  ac6num  8907  gchdomtri  9053  canth4  9071  gchpwdom  9094  gruima  9226  grudomon  9241  prn0  9413  distrlem4pr  9450  prlem934  9457  addcan  9816  addcan2  9817  ltmul1a  10453  supmul1  10576  uzsupss  11256  xaddass  11535  xleadd1a  11539  xlesubadd  11549  xmulass  11573  xlemul2a  11575  xadddilem  11580  xadddi  11581  ixxdisj  11650  ixxun  11651  ixxlb  11657  ixxlbOLD  11658  icoshftf1o  11753  icodisj  11755  lincmb01cmp  11773  iccf1o  11774  ssfzoulel  12002  modaddmulmod  12153  ltexp2a  12321  leexp2  12324  ltexp2r  12326  exple1  12329  expnlbnd2  12400  ccatass  12719  ccatopth  12811  swrdccatin12lem2a  12826  repswccat  12873  2cshw  12897  repsco  12921  s2f1o  12980  limsupgle  13513  limsupgre  13520  limsupgreOLD  13521  addcn2  13635  mulcn2  13637  binomrisefac  14073  dvdsval2  14286  dvdsadd2b  14325  dvdsmod  14340  oexpneg  14346  sadass  14419  gcdass  14484  rplpwr  14495  rppwr  14496  lcmass  14544  coprmdvds2  14622  rpmulgcd2  14624  rpexp  14634  rpdvds  14638  coprmprod  14640  prmdiveq  14694  odzdvds  14700  coprimeprodsq2  14714  pythagtriplem3  14722  pythagtriplem4  14723  pcdvdsb  14772  vdwnnlem1  14899  0ram  14932  ramz2  14936  ramub1lem1  14938  mremre  15452  mrieqv2d  15487  lubss  16309  lubun  16311  clatleglb  16314  clatglbss  16315  mrelatglb  16372  isnsgrp  16473  issubmnd  16506  gsumccat  16567  frmdss2  16589  nmzsubg  16800  ghmnsgima  16848  gsmsymgreqlem1  17013  psgnunilem4  17080  odmodnn0  17122  odnncl  17127  odmod  17128  oddvds  17129  odeq  17132  odmulgid  17134  odmulgeq  17137  odbezout  17138  odf1o1  17150  odf1o2  17151  odngen  17155  gexdvdsi  17161  pgpfi1  17173  odcau  17182  subgslw  17194  fislw  17203  lsmless1x  17222  lsmless2x  17223  lsmsubm  17231  lsmmod  17251  lsmmod2  17252  efgsfo  17315  odadd1  17412  odadd2  17413  odadd  17414  lsmcomx  17420  prdscmnd  17425  gsumconst  17493  srg1zr  17688  csrgbinom  17705  ring1eq0  17746  mulgass2  17755  cntzsubr  17966  isabvd  17974  0lmhm  18189  lmhmvsca  18194  reslmhm2b  18203  pwssplit1  18208  pwssplit2  18209  pwssplit3  18210  lbspss  18231  lspsnat  18294  lidldvgen  18405  issubassa  18474  evlsval2  18669  coe1subfv  18785  coe1sclmul  18801  coe1sclmul2  18803  xrsdsreclblem  18940  cssmre  19178  obs2ss  19214  uvcresum  19273  frlmsslsp  19276  frlmup4  19281  lindff1  19300  f1lindf  19302  lsslindf  19310  islindf4  19318  mpt2matmul  19393  mamutpos  19405  scmatscmide  19454  mavmulsolcl  19498  mulmarep1gsum2  19521  mdetdiaglem  19545  mdetdiag  19546  mdetunilem1  19559  mdetunilem3  19561  mdetunilem9  19567  maducoeval2  19587  madurid  19591  slesolinvbi  19628  cramerimplem1  19630  cramerlem1  19634  cramer  19638  cpmatel2  19659  m2cpm  19687  m2pmfzmap  19693  m2cpminvid2lem  19700  m2cpminvid2  19701  decpmatmul  19718  pmatcollpw1lem2  19721  pmatcollpw1  19722  pmatcollpw2lem  19723  pmatcollpwfi  19728  pm2mpcl  19743  mply1topmatcl  19751  mp2pm2mplem2  19753  mp2pm2mplem4  19755  mp2pm2mplem5  19756  mp2pm2mp  19757  pm2mpghmlem2  19758  pm2mpghmlem1  19759  chfacfisfcpmat  19801  topssnei  20062  cnconst2  20221  cnpresti  20226  cnprest2  20228  cnpdis  20231  cnt0  20284  cnt1  20288  cnhaus  20292  sscmp  20342  hauscmp  20344  cnconn  20359  uncon  20366  finlocfin  20457  comppfsc  20469  kgen2ss  20492  ptpjopn  20549  prdstopn  20565  ptrescn  20576  qtopss  20652  kqfvima  20667  fbssint  20775  fbasrn  20821  filuni  20822  fmss  20883  rnelfm  20890  fmufil  20896  fmco  20898  flimss2  20909  flimss1  20910  flimrest  20920  cnpflf2  20937  flfcnp  20941  supnfcls  20957  fclsss1  20959  fclsss2  20960  isfcf  20971  subgntr  21043  opnsubg  21044  cldsubg  21047  ghmcnp  21051  ustuqtop1  21178  bldisj  21335  blgt0  21336  bl2in  21337  blss2ps  21340  blss2  21341  blssps  21361  blss  21362  xmetresbl  21374  lpbl  21440  blcld  21442  stdbdmopn  21455  metcnp3  21477  metcnp  21478  metcnp2  21479  txmetcnp  21484  blval2  21499  nmoix  21652  nmoi2  21653  nmotri  21662  metdsge  21768  metdseq0  21773  iocopnst  21855  xrhmeo  21861  nmhmcn  22018  cphsqrtcl2  22048  cphsqrtcl3  22049  pjth  22265  ovoliunlem2  22325  volun  22366  mbfimaopn2  22481  iblconst  22643  limcvallem  22694  dvfval  22720  dvcnp2  22742  dvcn  22743  deg1mul3le  22933  deg1tmle  22934  dvdsq1p  22977  ig1peu  22988  ig1pdvds  22993  ply1term  23017  coeid3  23053  dgrmulc  23084  dvply1  23096  aaliou2  23152  efcvx  23260  tanord  23343  eflogeq  23407  logdivlti  23425  logccv  23464  recxpcl  23476  cxplea  23497  cxpeq  23553  ang180  23599  isosctrlem2  23604  cxp2lim  23758  amgm  23772  muval1  23914  dvdssqf  23919  mumullem2  23961  mumul  23962  bcmono  24059  lgsneg  24101  lgsdilem  24104  lgsdirprm  24111  lgsdir  24112  lgsdi  24114  lgsne0  24115  brbtwn2  24772  colinearalglem1  24773  colinearalg  24777  axcgrtr  24782  axsegconlem8  24791  axsegconlem9  24792  axsegconlem10  24793  axcontlem2  24832  axcontlem10  24840  cyclispthon  25197  wwlknext  25288  clwlkisclwwlklem0  25352  erclwwlksym  25378  eleclclwwlknlem2  25382  erclwwlkneqlen  25388  erclwwlknsym  25390  vdgrfval  25459  nbhashuvtx1  25479  usgreghash2spot  25633  extwwlkfablem2  25642  numclwwlk3lem  25672  frgraregord13  25683  gxcom  25833  gxnn0add  25838  nvmul0or  26109  ipval2lem2  26176  ipval2lem5  26182  lnoadd  26235  lnosub  26236  lnomul  26237  shless  26838  shlej1  26839  kbmul  27434  homco2  27456  kbass2  27596  eliccelico  28186  elicoelioo  28187  iocinioc2  28188  iocinif  28190  difioo  28191  xrge0adddir  28284  xrge0npcan  28286  isarchi2  28331  archiabl  28344  rhmdvdsr  28411  pstmfval  28529  fmcncfil  28567  zrhnm  28603  qqhnm  28624  nexple  28661  volfiniune  28883  dya2iocnrect  28933  probinc  29071  cndprob01  29085  signswmnd  29225  bnj517  29475  cvmsss2  29776  cvmlift2lem10  29814  br6  30175  funsseq  30187  frrlem4  30295  cgrtriv  30545  5segofs  30549  btwnouttr2  30565  btwnxfr  30599  lineext  30619  btwnconn1lem13  30642  brsegle2  30652  nn0prpwlem  30754  blbnd  31813  ismtyima  31829  rrndstprj2  31857  ghomdiv  31876  grpokerinj  31877  lsatfixedN  32274  lssat  32281  lshpkrlem4  32378  cvrcon3b  32542  atlen0  32575  atcvreq0  32579  atnle  32582  atlatmstc  32584  atlatle  32585  cvlcvr1  32604  hlsupr2  32651  hlrelat2  32667  cvrexchlem  32683  lnnat  32691  atcvrj2b  32696  3dimlem3  32725  3dim1  32731  1cvrjat  32739  llni  32772  llni2  32776  llnexatN  32785  2llnmat  32788  lplni  32796  2atnelpln  32808  llncvrlpln2  32821  2llnmj  32824  lplnexatN  32827  lplnexllnN  32828  2llnm3N  32833  lvoli  32839  lvoli3  32841  lvolnle3at  32846  islvol2aN  32856  4atlem4a  32863  4atlem4b  32864  4atlem11  32873  lplncvrlvol2  32879  2lplnmj  32886  islinei  33004  linepmap  33039  lnjatN  33044  lncvrat  33046  lncmp  33047  elpaddn0  33064  elpaddatriN  33067  elpaddat  33068  paddcom  33077  paddss2  33082  paddss12  33083  paddasslem4  33087  paddasslem9  33092  paddasslem10  33093  pmodl42N  33115  pmapjoin  33116  llnmod1i2  33124  polcon2bN  33184  pclfinclN  33214  poml4N  33217  poml6N  33219  osumcllem1N  33220  osumcllem2N  33221  osumcllem11N  33230  osumclN  33231  pmapojoinN  33232  pexmidlem2N  33235  pexmidlem3N  33236  pexmidlem4N  33237  pexmidlem6N  33239  pexmidlem7N  33240  pl42lem2N  33244  pl42lem3N  33245  pl42lem4N  33246  pl42N  33247  lhprelat3N  33304  4atex  33340  lauteq  33359  lautco  33361  ltrncoidN  33392  ltrneq2  33412  ltrnideq  33440  trlnle  33451  trlval3  33452  cdlemc  33462  cdlemd9  33471  cdlemd  33472  cdleme21j  33602  cdleme21  33603  cdleme29ex  33640  cdlemefr27cl  33669  cdlemefs27cl  33679  cdleme32d  33710  cdleme32f  33712  cdleme35h2  33723  cdleme40m  33733  cdleme17d3  33762  cdleme48fvg  33766  cdlemeg46fvcl  33772  cdlemeg46fgN  33800  cdleme48fgv  33804  cdleme50trn3  33819  cdlemb3  33872  cdlemg8  33897  cdlemg11a  33903  cdlemg15a  33921  cdlemg15  33922  cdlemg16  33923  cdlemg16z  33925  cdlemg17dN  33929  cdlemg24  33954  cdlemg37  33955  cdlemg29  33971  cdlemg33b  33973  cdlemg38  33981  cdlemg40  33983  trlco  33993  cdlemg44b  33998  ltrncom  34004  trljco  34006  tendococl  34038  tendoplcl  34047  tendoplcom  34048  cdlemj2  34088  tendoid0  34091  tendo1ne0  34094  cdlemk25-3  34170  cdlemk36  34179  cdlemkid4  34200  cdlemk19x  34209  cdlemk53  34223  cdlemk56  34237  cdleml5N  34246  tendospcanN  34290  cdlemm10N  34385  dihord6apre  34523  dihord  34531  dihmeetlem1N  34557  dihglblem2N  34561  dihmeetlem2N  34566  dihmeetbN  34570  dihmeetlem5  34575  dihmeetlem6  34576  dihmeetlem7N  34577  dihmeetlem10N  34583  dihmeetlem12N  34585  dihmeetlem16N  34589  dihmeetlem17N  34590  dihmeetlem18N  34591  dihmeetALTN  34594  dihlspsnssN  34599  dvh3dim2  34715  dvh3dim3N  34716  lcfrlem16  34825  mapdrvallem2  34912  mapdh8ad  35046  hgmapvvlem3  35195  diophrw  35300  eldioph2lem1  35301  diophrex  35317  rencldnfi  35363  pellexlem2  35374  pellqrexplicit  35421  infmrgelbi  35422  pellfundglb  35429  pellfund14gap  35431  rmxycomplete  35461  congadd  35512  acongeq  35529  jm2.19  35544  jm2.23  35547  jm2.20nn  35548  jm2.27  35559  jm3.1  35571  lnmepi  35639  lmhmlnmsplit  35641  hbtlem2  35679  dgraa0p  35704  idomrootle  35758  hashgcdlem  35763  proot1hash  35766  iocunico  35784  iocinico  35785  relexpxpmin  35938  rfcnnnub  36987  uzwo4  37023  supxrge  37160  snunioo2  37181  iccintsng  37199  climsuse  37249  lptre2pt  37282  limcleqr  37287  0ellimcdiv  37292  dvnprodlem1  37380  volioc  37408  stoweidlem17  37436  stoweidlem19  37438  stoweidlem20  37439  stoweidlem22  37441  stoweidlem28  37447  stoweidlem34  37454  stoweidlem44  37464  stoweidlem60  37480  wallispilem3  37488  fourierdlem42  37570  fourierdlem48  37576  fourierdlem51  37579  fourierdlem54  37582  fourierdlem74  37602  fourierdlem77  37605  fourierdlem87  37615  fourierdlem97  37625  fzopredsuc  38100  oexpnegALTV  38186  oexpnegnz  38187  tgblthelfgott  38288  repswpfx  38357  eluzge0nn0  38392  fzoopth  38402  rmsupp0  38903  rmsuppss  38905  lincresunit3lem3  39017  lincresunit3lem2  39023  lindssnlvec  39029  fdivmptf  39103  refdivmptf  39104  elbigolo1  39119
  Copyright terms: Public domain W3C validator