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

Theorem simpl2 985
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 982 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 462 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  simpll2  1021  simprl2  1027  simp1l2  1075  simp2l2  1081  simp3l2  1087  3anandirs  1314  rspc3ev  3072  brcogw  4995  weniso  6032  ofmpteq  6327  tfisi  6458  smogt  6814  smorndom  6815  omeulem1  7009  nnmord  7059  nnmword  7060  difsnen  7381  enfixsn  7408  mapunen  7468  ac6sfi  7544  ordiso2  7717  wemaplem2  7749  wemapso  7753  wemapso2lem  7755  en2eqpr  8162  acndom  8209  infmap2  8375  cflim2  8420  cfsmolem  8427  coftr  8430  fin23lem26  8482  isf32lem9  8518  fin1a2lem9  8565  fin1a2lem10  8566  ac6num  8636  gchdomtri  8784  canth4  8802  gchpwdom  8825  gruima  8957  grudomon  8972  prn0  9146  distrlem4pr  9183  prlem934  9190  addcan  9541  addcan2  9542  ltmul1a  10166  ledivmulOLD  10194  supmul1  10283  uzsupss  10935  xaddass  11200  xleadd1a  11204  xlesubadd  11214  xmulass  11238  xlemul2a  11240  xadddilem  11245  xadddi  11246  ixxdisj  11303  ixxun  11304  ixxlb  11310  icoshftf1o  11395  icodisj  11397  lincmb01cmp  11415  iccf1o  11416  ssfzoulel  11605  modaddmulmod  11749  ltexp2a  11899  leexp2  11902  ltexp2r  11904  exple1  11907  expnlbnd2  11979  ccatass  12270  swrdnd  12310  ccatopth  12348  swrdccatin12lem2a  12360  repswccat  12407  2cshw  12431  repsco  12451  s2f1o  12510  limsupgle  12939  limsupgre  12943  addcn2  13055  mulcn2  13057  dvdsval2  13521  dvdsadd2b  13558  dvdsmod  13573  oexpneg  13578  sadass  13650  gcdass  13712  rplpwr  13723  rppwr  13724  coprmdvds2  13772  rpmulgcd2  13774  rpexp  13789  rpdvds  13793  prmdiveq  13844  odzdvds  13850  coprimeprodsq2  13860  pythagtriplem3  13868  pythagtriplem4  13869  pcdvdsb  13918  vdwnnlem1  14039  0ram  14064  ramz2  14068  ramub1lem1  14070  mremre  14525  mrieqv2d  14560  lubss  15274  lubun  15276  clatleglb  15279  clatglbss  15280  mrelatglb  15337  issubmnd  15432  gsumccat  15499  frmdss2  15521  nmzsubg  15702  ghmnsgima  15750  gsmsymgreqlem1  15915  psgnunilem4  15983  odmodnn0  16023  odnncl  16028  odmod  16029  oddvds  16030  odeq  16033  odmulgid  16035  odmulgeq  16038  odbezout  16039  odf1o1  16051  odf1o2  16052  odngen  16056  gexdvdsi  16062  pgpfi1  16074  odcau  16083  subgslw  16095  fislw  16104  lsmless1x  16123  lsmless2x  16124  lsmsubm  16132  lsmmod  16152  lsmmod2  16153  efgsfo  16216  odadd1  16310  odadd2  16311  odadd  16312  lsmcomx  16318  prdscmnd  16323  gsumconst  16406  rng1eq0  16619  mulgass2  16627  cntzsubr  16821  isabvd  16829  0lmhm  17043  lmhmvsca  17048  reslmhm2b  17057  pwssplit1  17062  pwssplit2  17063  pwssplit3  17064  lbspss  17085  lspsnat  17148  lidldvgen  17259  issubassa  17317  coe1subfv  17618  coe1sclmul  17633  coe1sclmul2  17635  xrsdsreclblem  17703  cssmre  17960  obs2ss  17996  uvcresum  18060  frlmsslsp  18065  frlmsslspOLD  18066  frlmup4  18071  lindff1  18091  f1lindf  18093  lsslindf  18101  islindf4  18109  mamutpos  18185  mavmulsolcl  18204  mdetunilem1  18260  mdetunilem3  18262  mdetunilem9  18268  maducoeval2  18288  madurid  18292  slesolinvbi  18329  cramerimplem1  18331  cramerlem1  18335  cramer  18339  topssnei  18570  cnconst2  18729  cnpresti  18734  cnprest2  18736  cnpdis  18739  cnt0  18792  cnt1  18796  cnhaus  18800  sscmp  18850  hauscmp  18852  cnconn  18868  uncon  18875  kgen2ss  18970  ptpjopn  19027  prdstopn  19043  ptrescn  19054  qtopss  19130  kqfvima  19145  fbssint  19253  fbasrn  19299  filuni  19300  fmss  19361  rnelfm  19368  fmufil  19374  fmco  19376  flimss2  19387  flimss1  19388  flimrest  19398  cnpflf2  19415  flfcnp  19419  supnfcls  19435  fclsss1  19437  fclsss2  19438  isfcf  19449  subgntr  19519  opnsubg  19520  cldsubg  19523  ghmcnp  19527  ustuqtop1  19658  bldisj  19815  blgt0  19816  bl2in  19817  blss2ps  19820  blss2  19821  blssps  19841  blss  19842  xmetresbl  19854  lpbl  19920  blcld  19922  stdbdmopn  19935  metcnp3  19957  metcnp  19958  metcnp2  19959  txmetcnp  19964  blval2  19992  nmoix  20150  nmoi2  20151  nmotri  20160  metdsge  20267  metdseq0  20272  iocopnst  20354  xrhmeo  20360  nmhmcn  20517  cphsqrcl2  20547  cphsqrcl3  20548  pjth  20768  ovoliunlem2  20828  volun  20868  mbfimaopn2  20977  iblconst  21137  limcvallem  21188  dvfval  21214  dvcnp2  21236  dvcn  21237  evlsval2  21372  deg1mul3le  21473  deg1tmle  21474  dvdsq1p  21517  ig1peu  21528  ig1pdvds  21533  ply1term  21557  coeid3  21593  dgrmulc  21623  dvply1  21635  aaliou2  21691  efcvx  21799  tanord  21879  eflogeq  21935  logdivlti  21954  logccv  21993  recxpcl  22005  cxplea  22026  cxpeq  22080  ang180  22095  isosctrlem2  22102  cxp2lim  22255  amgm  22269  muval1  22356  dvdssqf  22361  mumullem2  22403  mumul  22404  bcmono  22501  lgsneg  22543  lgsdilem  22546  lgsdirprm  22553  lgsdir  22554  lgsdi  22556  lgsne0  22557  brbtwn2  22974  colinearalglem1  22975  colinearalg  22979  axcgrtr  22984  axsegconlem8  22993  axsegconlem9  22994  axsegconlem10  22995  axcontlem2  23034  axcontlem10  23042  cyclispthon  23342  vdgrfval  23388  gxcom  23579  gxnn0add  23584  nvmul0or  23855  ipval2lem2  23922  ipval2lem5  23928  lnoadd  23981  lnosub  23982  lnomul  23983  shless  24585  shlej1  24586  kbmul  25182  homco2  25204  kbass2  25344  eliccelico  25890  elicoelioo  25891  iocinioc2  25892  iocinif  25894  difioo  25895  xrge0adddir  25979  xrge0npcan  25981  isarchi2  26026  archiabl  26039  rhmdvdsr  26139  pstmfval  26177  fmcncfil  26215  zrhnm  26252  qqhnm  26273  nexple  26302  volfiniune  26500  dya2iocnrect  26550  probinc  26652  cndprob01  26666  signswmnd  26806  cvmsss2  27011  cvmlift2lem10  27049  binomrisefac  27392  br6  27414  funsseq  27427  frrlem4  27618  cgrtriv  27880  5segofs  27884  btwnouttr2  27900  btwnxfr  27934  lineext  27954  btwnconn1lem13  27977  brsegle2  27987  nn0prpwlem  28361  finlocfin  28415  comppfsc  28423  blbnd  28530  ismtyima  28546  rrndstprj2  28574  ghomdiv  28593  grpokerinj  28594  diophrw  28942  eldioph2lem1  28943  diophrex  28959  rencldnfi  29005  pellexlem2  29016  pellqrexplicit  29063  infmrgelbi  29064  pellfundglb  29071  pellfund14gap  29073  rmxycomplete  29103  congadd  29154  acongeq  29171  jm2.19  29187  jm2.23  29190  jm2.20nn  29191  jm2.27  29202  jm3.1  29214  lnmepi  29283  lmhmlnmsplit  29285  hbtlem2  29325  dgraa0p  29351  idomrootle  29405  hashgcdlem  29410  proot1hash  29413  iocunico  29431  iocinico  29432  rfcnnnub  29603  climsuse  29627  stoweidlem17  29658  stoweidlem19  29660  stoweidlem20  29661  stoweidlem22  29663  stoweidlem28  29669  stoweidlem34  29675  stoweidlem44  29685  stoweidlem60  29701  wallispilem3  29708  eluzge0nn0  30035  fzoopth  30059  wwlknext  30202  clwlkisclwwlklem0  30296  erclwwlksym  30330  eleclclwwlknlem2  30337  erclwwlkneqlen  30344  erclwwlknsym  30346  nbhashuvtx1  30379  usgreghash2spot  30508  extwwlkfablem2  30517  numclwwlk3lem  30547  frgraregord13  30558  mpt2sn  30568  rmsupp0  30612  rmsuppss  30614  lincresunit3lem3  30717  lincresunit3lem2  30723  lindssnlvec  30729  bnj517  31580  lsatfixedN  32227  lssat  32234  lshpkrlem4  32331  cvrcon3b  32495  atlen0  32528  atcvreq0  32532  atnle  32535  atlatmstc  32537  atlatle  32538  cvlcvr1  32557  hlsupr2  32604  hlrelat2  32620  cvrexchlem  32636  lnnat  32644  atcvrj2b  32649  3dimlem3  32678  3dim1  32684  1cvrjat  32692  llni  32725  llni2  32729  llnexatN  32738  2llnmat  32741  lplni  32749  2atnelpln  32761  llncvrlpln2  32774  2llnmj  32777  lplnexatN  32780  lplnexllnN  32781  2llnm3N  32786  lvoli  32792  lvoli3  32794  lvolnle3at  32799  islvol2aN  32809  4atlem4a  32816  4atlem4b  32817  4atlem11  32826  lplncvrlvol2  32832  2lplnmj  32839  islinei  32957  linepmap  32992  lnjatN  32997  lncvrat  32999  lncmp  33000  elpaddn0  33017  elpaddatriN  33020  elpaddat  33021  paddcom  33030  paddss2  33035  paddss12  33036  paddasslem4  33040  paddasslem9  33045  paddasslem10  33046  pmodl42N  33068  pmapjoin  33069  llnmod1i2  33077  polcon2bN  33137  pclfinclN  33167  poml4N  33170  poml6N  33172  osumcllem1N  33173  osumcllem2N  33174  osumcllem11N  33183  osumclN  33184  pmapojoinN  33185  pexmidlem2N  33188  pexmidlem3N  33189  pexmidlem4N  33190  pexmidlem6N  33192  pexmidlem7N  33193  pl42lem2N  33197  pl42lem3N  33198  pl42lem4N  33199  pl42N  33200  lhprelat3N  33257  4atex  33293  lauteq  33312  lautco  33314  ltrncoidN  33345  ltrneq2  33365  ltrnideq  33392  trlnle  33403  trlval3  33404  cdlemc  33414  cdlemd9  33423  cdlemd  33424  cdleme21j  33553  cdleme21  33554  cdleme29ex  33591  cdlemefr27cl  33620  cdlemefs27cl  33630  cdleme32d  33661  cdleme32f  33663  cdleme35h2  33674  cdleme40m  33684  cdleme17d3  33713  cdleme48fvg  33717  cdlemeg46fvcl  33723  cdlemeg46fgN  33751  cdleme48fgv  33755  cdleme50trn3  33770  cdlemb3  33823  cdlemg8  33848  cdlemg11a  33854  cdlemg15a  33872  cdlemg15  33873  cdlemg16  33874  cdlemg16z  33876  cdlemg17dN  33880  cdlemg24  33905  cdlemg37  33906  cdlemg29  33922  cdlemg33b  33924  cdlemg38  33932  cdlemg40  33934  trlco  33944  cdlemg44b  33949  ltrncom  33955  trljco  33957  tendococl  33989  tendoplcl  33998  tendoplcom  33999  cdlemj2  34039  tendoid0  34042  tendo1ne0  34045  cdlemk25-3  34121  cdlemk36  34130  cdlemkid4  34151  cdlemk19x  34160  cdlemk53  34174  cdlemk56  34188  cdleml5N  34197  tendospcanN  34241  cdlemm10N  34336  dihord6apre  34474  dihord  34482  dihmeetlem1N  34508  dihglblem2N  34512  dihmeetlem2N  34517  dihmeetbN  34521  dihmeetlem5  34526  dihmeetlem6  34527  dihmeetlem7N  34528  dihmeetlem10N  34534  dihmeetlem12N  34536  dihmeetlem16N  34540  dihmeetlem17N  34541  dihmeetlem18N  34542  dihmeetALTN  34545  dihlspsnssN  34550  dvh3dim2  34666  dvh3dim3N  34667  lcfrlem16  34776  mapdrvallem2  34863  mapdh8ad  34997  hgmapvvlem3  35146
  Copyright terms: Public domain W3C validator