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

Theorem simpl2 1001
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 998 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 465 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 974
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 185  df-an 371  df-3an 976
This theorem is referenced by:  simpll2  1037  simprl2  1043  simp1l2  1091  simp2l2  1097  simp3l2  1103  3anandirs  1332  rspc3ev  3209  brcogw  5161  weniso  6235  ofmpteq  6543  tfisi  6678  mpt2sn  6876  smogt  7040  smorndom  7041  omeulem1  7233  nnmord  7283  nnmword  7284  difsnen  7601  enfixsn  7628  mapunen  7688  ac6sfi  7766  ordiso2  7943  wemaplem2  7975  wemapso  7979  wemapso2lem  7981  en2eqpr  8388  acndom  8435  infmap2  8601  cflim2  8646  cfsmolem  8653  coftr  8656  fin23lem26  8708  isf32lem9  8744  fin1a2lem9  8791  fin1a2lem10  8792  ac6num  8862  gchdomtri  9010  canth4  9028  gchpwdom  9051  gruima  9183  grudomon  9198  prn0  9370  distrlem4pr  9407  prlem934  9414  addcan  9767  addcan2  9768  ltmul1a  10398  ledivmulOLD  10426  supmul1  10515  uzsupss  11185  xaddass  11452  xleadd1a  11456  xlesubadd  11466  xmulass  11490  xlemul2a  11492  xadddilem  11497  xadddi  11498  ixxdisj  11555  ixxun  11556  ixxlb  11562  icoshftf1o  11654  icodisj  11656  lincmb01cmp  11674  iccf1o  11675  ssfzoulel  11888  modaddmulmod  12035  ltexp2a  12199  leexp2  12202  ltexp2r  12204  exple1  12207  expnlbnd2  12279  ccatass  12587  swrdnd  12639  ccatopth  12677  swrdccatin12lem2a  12692  repswccat  12739  2cshw  12763  repsco  12787  s2f1o  12846  limsupgle  13282  limsupgre  13286  addcn2  13398  mulcn2  13400  dvdsval2  13971  dvdsadd2b  14010  dvdsmod  14025  oexpneg  14031  sadass  14103  gcdass  14165  rplpwr  14176  rppwr  14177  coprmdvds2  14226  rpmulgcd2  14228  rpexp  14243  rpdvds  14247  prmdiveq  14298  odzdvds  14304  coprimeprodsq2  14316  pythagtriplem3  14324  pythagtriplem4  14325  pcdvdsb  14374  vdwnnlem1  14495  0ram  14520  ramz2  14524  ramub1lem1  14526  mremre  14983  mrieqv2d  15018  lubss  15730  lubun  15732  clatleglb  15735  clatglbss  15736  mrelatglb  15793  isnsgrp  15894  issubmnd  15927  gsumccat  15988  frmdss2  16010  nmzsubg  16221  ghmnsgima  16269  gsmsymgreqlem1  16434  psgnunilem4  16501  odmodnn0  16543  odnncl  16548  odmod  16549  oddvds  16550  odeq  16553  odmulgid  16555  odmulgeq  16558  odbezout  16559  odf1o1  16571  odf1o2  16572  odngen  16576  gexdvdsi  16582  pgpfi1  16594  odcau  16603  subgslw  16615  fislw  16624  lsmless1x  16643  lsmless2x  16644  lsmsubm  16652  lsmmod  16672  lsmmod2  16673  efgsfo  16736  odadd1  16833  odadd2  16834  odadd  16835  lsmcomx  16841  prdscmnd  16846  gsumconst  16933  srg1zr  17159  csrgbinom  17176  ring1eq0  17217  mulgass2  17226  cntzsubr  17440  isabvd  17448  0lmhm  17665  lmhmvsca  17670  reslmhm2b  17679  pwssplit1  17684  pwssplit2  17685  pwssplit3  17686  lbspss  17707  lspsnat  17770  lidldvgen  17882  issubassa  17952  evlsval2  18168  coe1subfv  18286  coe1sclmul  18302  coe1sclmul2  18304  xrsdsreclblem  18443  cssmre  18702  obs2ss  18738  uvcresum  18802  frlmsslsp  18807  frlmsslspOLD  18808  frlmup4  18813  lindff1  18833  f1lindf  18835  lsslindf  18843  islindf4  18851  mpt2matmul  18926  mamutpos  18938  scmatscmide  18987  mavmulsolcl  19031  mulmarep1gsum2  19054  mdetdiaglem  19078  mdetdiag  19079  mdetunilem1  19092  mdetunilem3  19094  mdetunilem9  19100  maducoeval2  19120  madurid  19124  slesolinvbi  19161  cramerimplem1  19163  cramerlem1  19167  cramer  19171  cpmatel2  19192  m2cpm  19220  m2pmfzmap  19226  m2cpminvid2lem  19233  m2cpminvid2  19234  decpmatmul  19251  pmatcollpw1lem2  19254  pmatcollpw1  19255  pmatcollpw2lem  19256  pmatcollpwfi  19261  pm2mpcl  19276  mply1topmatcl  19284  mp2pm2mplem2  19286  mp2pm2mplem4  19288  mp2pm2mplem5  19289  mp2pm2mp  19290  pm2mpghmlem2  19291  pm2mpghmlem1  19292  chfacfisfcpmat  19334  topssnei  19603  cnconst2  19762  cnpresti  19767  cnprest2  19769  cnpdis  19772  cnt0  19825  cnt1  19829  cnhaus  19833  sscmp  19883  hauscmp  19885  cnconn  19901  uncon  19908  finlocfin  19999  comppfsc  20011  kgen2ss  20034  ptpjopn  20091  prdstopn  20107  ptrescn  20118  qtopss  20194  kqfvima  20209  fbssint  20317  fbasrn  20363  filuni  20364  fmss  20425  rnelfm  20432  fmufil  20438  fmco  20440  flimss2  20451  flimss1  20452  flimrest  20462  cnpflf2  20479  flfcnp  20483  supnfcls  20499  fclsss1  20501  fclsss2  20502  isfcf  20513  subgntr  20583  opnsubg  20584  cldsubg  20587  ghmcnp  20591  ustuqtop1  20722  bldisj  20879  blgt0  20880  bl2in  20881  blss2ps  20884  blss2  20885  blssps  20905  blss  20906  xmetresbl  20918  lpbl  20984  blcld  20986  stdbdmopn  20999  metcnp3  21021  metcnp  21022  metcnp2  21023  txmetcnp  21028  blval2  21056  nmoix  21214  nmoi2  21215  nmotri  21224  metdsge  21331  metdseq0  21336  iocopnst  21418  xrhmeo  21424  nmhmcn  21581  cphsqrtcl2  21611  cphsqrtcl3  21612  pjth  21832  ovoliunlem2  21892  volun  21933  mbfimaopn2  22042  iblconst  22202  limcvallem  22253  dvfval  22279  dvcnp2  22301  dvcn  22302  deg1mul3le  22495  deg1tmle  22496  dvdsq1p  22539  ig1peu  22550  ig1pdvds  22555  ply1term  22579  coeid3  22615  dgrmulc  22646  dvply1  22658  aaliou2  22714  efcvx  22822  tanord  22903  eflogeq  22964  logdivlti  22983  logccv  23022  recxpcl  23034  cxplea  23055  cxpeq  23109  ang180  23124  isosctrlem2  23131  cxp2lim  23284  amgm  23298  muval1  23385  dvdssqf  23390  mumullem2  23432  mumul  23433  bcmono  23530  lgsneg  23572  lgsdilem  23575  lgsdirprm  23582  lgsdir  23583  lgsdi  23585  lgsne0  23586  brbtwn2  24186  colinearalglem1  24187  colinearalg  24191  axcgrtr  24196  axsegconlem8  24205  axsegconlem9  24206  axsegconlem10  24207  axcontlem2  24246  axcontlem10  24254  cyclispthon  24611  wwlknext  24702  clwlkisclwwlklem0  24766  erclwwlksym  24792  eleclclwwlknlem2  24796  erclwwlkneqlen  24802  erclwwlknsym  24804  vdgrfval  24873  nbhashuvtx1  24893  usgreghash2spot  25047  extwwlkfablem2  25056  numclwwlk3lem  25086  frgraregord13  25097  gxcom  25249  gxnn0add  25254  nvmul0or  25525  ipval2lem2  25592  ipval2lem5  25598  lnoadd  25651  lnosub  25652  lnomul  25653  shless  26255  shlej1  26256  kbmul  26852  homco2  26874  kbass2  27014  eliccelico  27566  elicoelioo  27567  iocinioc2  27568  iocinif  27570  difioo  27571  xrge0adddir  27660  xrge0npcan  27662  isarchi2  27707  archiabl  27720  rhmdvdsr  27786  pstmfval  27853  fmcncfil  27891  zrhnm  27928  qqhnm  27949  nexple  27983  volfiniune  28180  dya2iocnrect  28230  probinc  28338  cndprob01  28352  signswmnd  28492  cvmsss2  28697  cvmlift2lem10  28735  binomrisefac  29140  br6  29162  funsseq  29175  frrlem4  29366  cgrtriv  29628  5segofs  29632  btwnouttr2  29648  btwnxfr  29682  lineext  29702  btwnconn1lem13  29725  brsegle2  29735  nn0prpwlem  30116  blbnd  30259  ismtyima  30275  rrndstprj2  30303  ghomdiv  30322  grpokerinj  30323  diophrw  30668  eldioph2lem1  30669  diophrex  30685  rencldnfi  30731  pellexlem2  30742  pellqrexplicit  30789  infmrgelbi  30790  pellfundglb  30797  pellfund14gap  30799  rmxycomplete  30829  congadd  30880  acongeq  30897  jm2.19  30911  jm2.23  30914  jm2.20nn  30915  jm2.27  30926  jm3.1  30938  lnmepi  31007  lmhmlnmsplit  31009  hbtlem2  31049  dgraa0p  31074  idomrootle  31128  hashgcdlem  31133  proot1hash  31136  iocunico  31154  iocinico  31155  lcmass  31194  rfcnnnub  31365  snunioo2  31498  iccintsng  31517  climsuse  31568  lptre2pt  31600  limcleqr  31604  0ellimcdiv  31609  dvnprodlem1  31697  volioc  31725  stoweidlem17  31753  stoweidlem19  31755  stoweidlem20  31756  stoweidlem22  31758  stoweidlem28  31764  stoweidlem34  31770  stoweidlem44  31780  stoweidlem60  31796  wallispilem3  31803  fourierdlem42  31885  fourierdlem48  31891  fourierdlem51  31894  fourierdlem54  31897  fourierdlem74  31917  fourierdlem77  31920  fourierdlem87  31930  fourierdlem97  31940  eluzge0nn0  32283  fzoopth  32294  rmsupp0  32831  rmsuppss  32833  lincresunit3lem3  32945  lincresunit3lem2  32951  lindssnlvec  32957  bnj517  33811  lsatfixedN  34609  lssat  34616  lshpkrlem4  34713  cvrcon3b  34877  atlen0  34910  atcvreq0  34914  atnle  34917  atlatmstc  34919  atlatle  34920  cvlcvr1  34939  hlsupr2  34986  hlrelat2  35002  cvrexchlem  35018  lnnat  35026  atcvrj2b  35031  3dimlem3  35060  3dim1  35066  1cvrjat  35074  llni  35107  llni2  35111  llnexatN  35120  2llnmat  35123  lplni  35131  2atnelpln  35143  llncvrlpln2  35156  2llnmj  35159  lplnexatN  35162  lplnexllnN  35163  2llnm3N  35168  lvoli  35174  lvoli3  35176  lvolnle3at  35181  islvol2aN  35191  4atlem4a  35198  4atlem4b  35199  4atlem11  35208  lplncvrlvol2  35214  2lplnmj  35221  islinei  35339  linepmap  35374  lnjatN  35379  lncvrat  35381  lncmp  35382  elpaddn0  35399  elpaddatriN  35402  elpaddat  35403  paddcom  35412  paddss2  35417  paddss12  35418  paddasslem4  35422  paddasslem9  35427  paddasslem10  35428  pmodl42N  35450  pmapjoin  35451  llnmod1i2  35459  polcon2bN  35519  pclfinclN  35549  poml4N  35552  poml6N  35554  osumcllem1N  35555  osumcllem2N  35556  osumcllem11N  35565  osumclN  35566  pmapojoinN  35567  pexmidlem2N  35570  pexmidlem3N  35571  pexmidlem4N  35572  pexmidlem6N  35574  pexmidlem7N  35575  pl42lem2N  35579  pl42lem3N  35580  pl42lem4N  35581  pl42N  35582  lhprelat3N  35639  4atex  35675  lauteq  35694  lautco  35696  ltrncoidN  35727  ltrneq2  35747  ltrnideq  35775  trlnle  35786  trlval3  35787  cdlemc  35797  cdlemd9  35806  cdlemd  35807  cdleme21j  35937  cdleme21  35938  cdleme29ex  35975  cdlemefr27cl  36004  cdlemefs27cl  36014  cdleme32d  36045  cdleme32f  36047  cdleme35h2  36058  cdleme40m  36068  cdleme17d3  36097  cdleme48fvg  36101  cdlemeg46fvcl  36107  cdlemeg46fgN  36135  cdleme48fgv  36139  cdleme50trn3  36154  cdlemb3  36207  cdlemg8  36232  cdlemg11a  36238  cdlemg15a  36256  cdlemg15  36257  cdlemg16  36258  cdlemg16z  36260  cdlemg17dN  36264  cdlemg24  36289  cdlemg37  36290  cdlemg29  36306  cdlemg33b  36308  cdlemg38  36316  cdlemg40  36318  trlco  36328  cdlemg44b  36333  ltrncom  36339  trljco  36341  tendococl  36373  tendoplcl  36382  tendoplcom  36383  cdlemj2  36423  tendoid0  36426  tendo1ne0  36429  cdlemk25-3  36505  cdlemk36  36514  cdlemkid4  36535  cdlemk19x  36544  cdlemk53  36558  cdlemk56  36572  cdleml5N  36581  tendospcanN  36625  cdlemm10N  36720  dihord6apre  36858  dihord  36866  dihmeetlem1N  36892  dihglblem2N  36896  dihmeetlem2N  36901  dihmeetbN  36905  dihmeetlem5  36910  dihmeetlem6  36911  dihmeetlem7N  36912  dihmeetlem10N  36918  dihmeetlem12N  36920  dihmeetlem16N  36924  dihmeetlem17N  36925  dihmeetlem18N  36926  dihmeetALTN  36929  dihlspsnssN  36934  dvh3dim2  37050  dvh3dim3N  37051  lcfrlem16  37160  mapdrvallem2  37247  mapdh8ad  37381  hgmapvvlem3  37530
  Copyright terms: Public domain W3C validator