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

Theorem simpl2 992
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 989 . 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 965
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 967
This theorem is referenced by:  simpll2  1028  simprl2  1034  simp1l2  1082  simp2l2  1088  simp3l2  1094  3anandirs  1322  rspc3ev  3180  brcogw  5106  weniso  6144  ofmpteq  6438  tfisi  6569  smogt  6928  smorndom  6929  omeulem1  7121  nnmord  7171  nnmword  7172  difsnen  7493  enfixsn  7520  mapunen  7580  ac6sfi  7657  ordiso2  7830  wemaplem2  7862  wemapso  7866  wemapso2lem  7868  en2eqpr  8275  acndom  8322  infmap2  8488  cflim2  8533  cfsmolem  8540  coftr  8543  fin23lem26  8595  isf32lem9  8631  fin1a2lem9  8678  fin1a2lem10  8679  ac6num  8749  gchdomtri  8897  canth4  8915  gchpwdom  8938  gruima  9070  grudomon  9085  prn0  9259  distrlem4pr  9296  prlem934  9303  addcan  9654  addcan2  9655  ltmul1a  10279  ledivmulOLD  10307  supmul1  10396  uzsupss  11048  xaddass  11313  xleadd1a  11317  xlesubadd  11327  xmulass  11351  xlemul2a  11353  xadddilem  11358  xadddi  11359  ixxdisj  11416  ixxun  11417  ixxlb  11423  icoshftf1o  11509  icodisj  11511  lincmb01cmp  11529  iccf1o  11530  ssfzoulel  11722  modaddmulmod  11866  ltexp2a  12016  leexp2  12019  ltexp2r  12021  exple1  12024  expnlbnd2  12096  ccatass  12388  swrdnd  12428  ccatopth  12466  swrdccatin12lem2a  12478  repswccat  12525  2cshw  12549  repsco  12569  s2f1o  12628  limsupgle  13057  limsupgre  13061  addcn2  13173  mulcn2  13175  dvdsval2  13640  dvdsadd2b  13677  dvdsmod  13692  oexpneg  13697  sadass  13769  gcdass  13831  rplpwr  13842  rppwr  13843  coprmdvds2  13891  rpmulgcd2  13893  rpexp  13908  rpdvds  13912  prmdiveq  13963  odzdvds  13969  coprimeprodsq2  13979  pythagtriplem3  13987  pythagtriplem4  13988  pcdvdsb  14037  vdwnnlem1  14158  0ram  14183  ramz2  14187  ramub1lem1  14189  mremre  14644  mrieqv2d  14679  lubss  15393  lubun  15395  clatleglb  15398  clatglbss  15399  mrelatglb  15456  issubmnd  15551  gsumccat  15621  frmdss2  15643  nmzsubg  15824  ghmnsgima  15872  gsmsymgreqlem1  16037  psgnunilem4  16105  odmodnn0  16147  odnncl  16152  odmod  16153  oddvds  16154  odeq  16157  odmulgid  16159  odmulgeq  16162  odbezout  16163  odf1o1  16175  odf1o2  16176  odngen  16180  gexdvdsi  16186  pgpfi1  16198  odcau  16207  subgslw  16219  fislw  16228  lsmless1x  16247  lsmless2x  16248  lsmsubm  16256  lsmmod  16276  lsmmod2  16277  efgsfo  16340  odadd1  16434  odadd2  16435  odadd  16436  lsmcomx  16442  prdscmnd  16447  gsumconst  16532  csrgbinom  16750  rng1eq0  16790  mulgass2  16798  cntzsubr  17003  isabvd  17011  0lmhm  17227  lmhmvsca  17232  reslmhm2b  17241  pwssplit1  17246  pwssplit2  17247  pwssplit3  17248  lbspss  17269  lspsnat  17332  lidldvgen  17443  issubassa  17501  evlsval2  17713  coe1subfv  17827  coe1sclmul  17843  coe1sclmul2  17845  xrsdsreclblem  17968  cssmre  18227  obs2ss  18263  uvcresum  18327  frlmsslsp  18332  frlmsslspOLD  18333  frlmup4  18338  lindff1  18358  f1lindf  18360  lsslindf  18368  islindf4  18376  mamutpos  18454  mavmulsolcl  18473  mdetdiaglem  18520  mdetdiag  18521  mdetunilem1  18534  mdetunilem3  18536  mdetunilem9  18542  maducoeval2  18562  madurid  18566  slesolinvbi  18603  cramerimplem1  18605  cramerlem1  18609  cramer  18613  topssnei  18844  cnconst2  19003  cnpresti  19008  cnprest2  19010  cnpdis  19013  cnt0  19066  cnt1  19070  cnhaus  19074  sscmp  19124  hauscmp  19126  cnconn  19142  uncon  19149  kgen2ss  19244  ptpjopn  19301  prdstopn  19317  ptrescn  19328  qtopss  19404  kqfvima  19419  fbssint  19527  fbasrn  19573  filuni  19574  fmss  19635  rnelfm  19642  fmufil  19648  fmco  19650  flimss2  19661  flimss1  19662  flimrest  19672  cnpflf2  19689  flfcnp  19693  supnfcls  19709  fclsss1  19711  fclsss2  19712  isfcf  19723  subgntr  19793  opnsubg  19794  cldsubg  19797  ghmcnp  19801  ustuqtop1  19932  bldisj  20089  blgt0  20090  bl2in  20091  blss2ps  20094  blss2  20095  blssps  20115  blss  20116  xmetresbl  20128  lpbl  20194  blcld  20196  stdbdmopn  20209  metcnp3  20231  metcnp  20232  metcnp2  20233  txmetcnp  20238  blval2  20266  nmoix  20424  nmoi2  20425  nmotri  20434  metdsge  20541  metdseq0  20546  iocopnst  20628  xrhmeo  20634  nmhmcn  20791  cphsqrcl2  20821  cphsqrcl3  20822  pjth  21042  ovoliunlem2  21102  volun  21142  mbfimaopn2  21251  iblconst  21411  limcvallem  21462  dvfval  21488  dvcnp2  21510  dvcn  21511  deg1mul3le  21704  deg1tmle  21705  dvdsq1p  21748  ig1peu  21759  ig1pdvds  21764  ply1term  21788  coeid3  21824  dgrmulc  21854  dvply1  21866  aaliou2  21922  efcvx  22030  tanord  22110  eflogeq  22166  logdivlti  22185  logccv  22224  recxpcl  22236  cxplea  22257  cxpeq  22311  ang180  22326  isosctrlem2  22333  cxp2lim  22486  amgm  22500  muval1  22587  dvdssqf  22592  mumullem2  22634  mumul  22635  bcmono  22732  lgsneg  22774  lgsdilem  22777  lgsdirprm  22784  lgsdir  22785  lgsdi  22787  lgsne0  22788  brbtwn2  23286  colinearalglem1  23287  colinearalg  23291  axcgrtr  23296  axsegconlem8  23305  axsegconlem9  23306  axsegconlem10  23307  axcontlem2  23346  axcontlem10  23354  cyclispthon  23654  vdgrfval  23700  gxcom  23891  gxnn0add  23896  nvmul0or  24167  ipval2lem2  24234  ipval2lem5  24240  lnoadd  24293  lnosub  24294  lnomul  24295  shless  24897  shlej1  24898  kbmul  25494  homco2  25516  kbass2  25656  eliccelico  26201  elicoelioo  26202  iocinioc2  26203  iocinif  26205  difioo  26206  xrge0adddir  26289  xrge0npcan  26291  isarchi2  26336  archiabl  26349  rhmdvdsr  26420  pstmfval  26457  fmcncfil  26495  zrhnm  26532  qqhnm  26553  nexple  26582  volfiniune  26780  dya2iocnrect  26830  probinc  26938  cndprob01  26952  signswmnd  27092  cvmsss2  27297  cvmlift2lem10  27335  binomrisefac  27679  br6  27701  funsseq  27714  frrlem4  27905  cgrtriv  28167  5segofs  28171  btwnouttr2  28187  btwnxfr  28221  lineext  28241  btwnconn1lem13  28264  brsegle2  28274  nn0prpwlem  28655  finlocfin  28709  comppfsc  28717  blbnd  28824  ismtyima  28840  rrndstprj2  28868  ghomdiv  28887  grpokerinj  28888  diophrw  29235  eldioph2lem1  29236  diophrex  29252  rencldnfi  29298  pellexlem2  29309  pellqrexplicit  29356  infmrgelbi  29357  pellfundglb  29364  pellfund14gap  29366  rmxycomplete  29396  congadd  29447  acongeq  29464  jm2.19  29480  jm2.23  29483  jm2.20nn  29484  jm2.27  29495  jm3.1  29507  lnmepi  29576  lmhmlnmsplit  29578  hbtlem2  29618  dgraa0p  29644  idomrootle  29698  hashgcdlem  29703  proot1hash  29706  iocunico  29724  iocinico  29725  rfcnnnub  29896  climsuse  29919  stoweidlem17  29950  stoweidlem19  29952  stoweidlem20  29953  stoweidlem22  29955  stoweidlem28  29961  stoweidlem34  29967  stoweidlem44  29977  stoweidlem60  29993  wallispilem3  30000  eluzge0nn0  30327  fzoopth  30351  wwlknext  30494  clwlkisclwwlklem0  30588  erclwwlksym  30622  eleclclwwlknlem2  30629  erclwwlkneqlen  30636  erclwwlknsym  30638  nbhashuvtx1  30671  usgreghash2spot  30800  extwwlkfablem2  30809  numclwwlk3lem  30839  frgraregord13  30850  mpt2sn  30861  rmsupp0  30919  rmsuppss  30921  scmatel  31010  lincresunit3lem3  31115  lincresunit3lem2  31121  lindssnlvec  31127  cpmatel2  31176  m2cpm  31204  m2pminv2lem  31212  m2pmfzmap  31218  pmatcollpw1dst  31228  pmatcollpw1lem5  31231  pmatcollpw1  31232  mply1topmatcl  31252  mp2pm2mplem2  31262  mp2pm2mplem4  31264  chfacfisfcpmat  31309  cpmadumatpolylem3  31337  bnj517  32178  lsatfixedN  32960  lssat  32967  lshpkrlem4  33064  cvrcon3b  33228  atlen0  33261  atcvreq0  33265  atnle  33268  atlatmstc  33270  atlatle  33271  cvlcvr1  33290  hlsupr2  33337  hlrelat2  33353  cvrexchlem  33369  lnnat  33377  atcvrj2b  33382  3dimlem3  33411  3dim1  33417  1cvrjat  33425  llni  33458  llni2  33462  llnexatN  33471  2llnmat  33474  lplni  33482  2atnelpln  33494  llncvrlpln2  33507  2llnmj  33510  lplnexatN  33513  lplnexllnN  33514  2llnm3N  33519  lvoli  33525  lvoli3  33527  lvolnle3at  33532  islvol2aN  33542  4atlem4a  33549  4atlem4b  33550  4atlem11  33559  lplncvrlvol2  33565  2lplnmj  33572  islinei  33690  linepmap  33725  lnjatN  33730  lncvrat  33732  lncmp  33733  elpaddn0  33750  elpaddatriN  33753  elpaddat  33754  paddcom  33763  paddss2  33768  paddss12  33769  paddasslem4  33773  paddasslem9  33778  paddasslem10  33779  pmodl42N  33801  pmapjoin  33802  llnmod1i2  33810  polcon2bN  33870  pclfinclN  33900  poml4N  33903  poml6N  33905  osumcllem1N  33906  osumcllem2N  33907  osumcllem11N  33916  osumclN  33917  pmapojoinN  33918  pexmidlem2N  33921  pexmidlem3N  33922  pexmidlem4N  33923  pexmidlem6N  33925  pexmidlem7N  33926  pl42lem2N  33930  pl42lem3N  33931  pl42lem4N  33932  pl42N  33933  lhprelat3N  33990  4atex  34026  lauteq  34045  lautco  34047  ltrncoidN  34078  ltrneq2  34098  ltrnideq  34125  trlnle  34136  trlval3  34137  cdlemc  34147  cdlemd9  34156  cdlemd  34157  cdleme21j  34286  cdleme21  34287  cdleme29ex  34324  cdlemefr27cl  34353  cdlemefs27cl  34363  cdleme32d  34394  cdleme32f  34396  cdleme35h2  34407  cdleme40m  34417  cdleme17d3  34446  cdleme48fvg  34450  cdlemeg46fvcl  34456  cdlemeg46fgN  34484  cdleme48fgv  34488  cdleme50trn3  34503  cdlemb3  34556  cdlemg8  34581  cdlemg11a  34587  cdlemg15a  34605  cdlemg15  34606  cdlemg16  34607  cdlemg16z  34609  cdlemg17dN  34613  cdlemg24  34638  cdlemg37  34639  cdlemg29  34655  cdlemg33b  34657  cdlemg38  34665  cdlemg40  34667  trlco  34677  cdlemg44b  34682  ltrncom  34688  trljco  34690  tendococl  34722  tendoplcl  34731  tendoplcom  34732  cdlemj2  34772  tendoid0  34775  tendo1ne0  34778  cdlemk25-3  34854  cdlemk36  34863  cdlemkid4  34884  cdlemk19x  34893  cdlemk53  34907  cdlemk56  34921  cdleml5N  34930  tendospcanN  34974  cdlemm10N  35069  dihord6apre  35207  dihord  35215  dihmeetlem1N  35241  dihglblem2N  35245  dihmeetlem2N  35250  dihmeetbN  35254  dihmeetlem5  35259  dihmeetlem6  35260  dihmeetlem7N  35261  dihmeetlem10N  35267  dihmeetlem12N  35269  dihmeetlem16N  35273  dihmeetlem17N  35274  dihmeetlem18N  35275  dihmeetALTN  35278  dihlspsnssN  35283  dvh3dim2  35399  dvh3dim3N  35400  lcfrlem16  35509  mapdrvallem2  35596  mapdh8ad  35730  hgmapvvlem3  35879
  Copyright terms: Public domain W3C validator