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

Theorem simpl2 962
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 959 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 453 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  simpll2  998  simprl2  1004  simp1l2  1052  simp2l2  1058  simp3l2  1064  3anandirs  1287  rspc3ev  3071  tfisi  4873  brcogw  5076  weniso  6111  smogt  6665  smorndom  6666  omeulem1  6861  nnmord  6911  nnmword  6912  difsnen  7226  mapunen  7312  ac6sfi  7387  ordiso2  7520  wemaplem2  7552  wemapso  7556  en2eqpr  7929  acndom  7970  infmap2  8136  cflim2  8181  cfsmolem  8188  coftr  8191  fin23lem26  8243  isf32lem9  8279  fin1a2lem9  8326  fin1a2lem10  8327  ac6num  8397  gchdomtri  8542  canth4  8560  gchpwdom  8583  gruima  8715  grudomon  8730  prn0  8904  distrlem4pr  8941  prlem934  8948  addcan  9288  addcan2  9289  ltmul1a  9897  ledivmulOLD  9922  supmul1  10011  uzsupss  10606  xaddass  10866  xleadd1a  10870  xlesubadd  10880  xmulass  10904  xlemul2a  10906  xadddilem  10911  xadddi  10912  ixxdisj  10969  ixxun  10970  ixxlb  10976  icoshftf1o  11058  icodisj  11060  lincmb01cmp  11076  iccf1o  11077  ltexp2a  11469  leexp2  11472  ltexp2r  11474  exple1  11477  expnlbnd2  11548  ccatass  11788  ccatopth  11814  s2f1o  11901  limsupgle  12309  limsupgre  12313  addcn2  12425  mulcn2  12427  dvdsval2  12893  dvdsadd2b  12930  dvdsmod  12944  oexpneg  12949  sadass  13021  gcdass  13083  rplpwr  13094  rppwr  13095  coprmdvds2  13141  rpmulgcd2  13143  rpexp  13158  rpdvds  13162  prmdiveq  13213  odzdvds  13219  coprimeprodsq2  13222  pythagtriplem3  13230  pythagtriplem4  13231  pcdvdsb  13280  vdwnnlem1  13401  0ram  13426  ramz2  13430  ramub1lem1  13432  mremre  13867  mrieqv2d  13902  lubss  14586  lubun  14588  clatleglb  14591  clatglbss  14592  mrelatglb  14648  issubmnd  14762  gsumccat  14825  frmdss2  14846  nmzsubg  15019  ghmnsgima  15067  odmodnn0  15216  odnncl  15221  odmod  15222  oddvds  15223  odeq  15226  odmulgid  15228  odmulgeq  15231  odbezout  15232  odf1o1  15244  odf1o2  15245  odngen  15249  gexdvdsi  15255  pgpfi1  15267  odcau  15276  subgslw  15288  fislw  15297  lsmless1x  15316  lsmless2x  15317  lsmsubm  15325  lsmmod  15345  lsmmod2  15346  efgsfo  15409  odadd1  15501  odadd2  15502  odadd  15503  lsmcomx  15509  prdscmnd  15514  gsumconst  15570  rng1eq0  15740  mulgass2  15748  cntzsubr  15938  isabvd  15946  0lmhm  16154  lmhmvsca  16159  reslmhm2b  16168  lbspss  16192  lspsnat  16255  lidldvgen  16364  issubassa  16421  coe1subfv  16697  coe1sclmul  16712  coe1sclmul2  16714  xrsdsreclblem  16782  cssmre  16958  obs2ss  16994  topssnei  17226  cnconst2  17385  cnpresti  17390  cnprest2  17392  cnpdis  17395  cnt0  17448  cnt1  17452  cnhaus  17456  sscmp  17506  hauscmp  17508  cnconn  17523  uncon  17530  kgen2ss  17625  ptpjopn  17682  prdstopn  17698  ptrescn  17709  qtopss  17785  kqfvima  17800  fbssint  17908  fbasrn  17954  filuni  17955  fmss  18016  rnelfm  18023  fmufil  18029  fmco  18031  flimss2  18042  flimss1  18043  flimrest  18053  cnpflf2  18070  flfcnp  18074  supnfcls  18090  fclsss1  18092  fclsss2  18093  isfcf  18104  subgntr  18174  opnsubg  18175  cldsubg  18178  ghmcnp  18182  ustuqtop1  18309  bldisj  18466  blgt0  18467  bl2in  18468  blss2ps  18471  blss2  18472  blssps  18492  blss  18493  xmetresbl  18505  lpbl  18571  blcld  18573  stdbdmopn  18586  metcnp3  18608  metcnp  18609  metcnp2  18610  txmetcnp  18615  blval2  18643  nmoix  18801  nmoi2  18802  nmotri  18811  metdsge  18917  metdseq0  18922  iocopnst  19003  xrhmeo  19009  nmhmcn  19166  cphsqrcl2  19187  cphsqrcl3  19188  pjth  19378  ovoliunlem2  19437  volun  19477  mbfimaopn2  19585  iblconst  19745  limcvallem  19796  dvfval  19822  dvcnp2  19844  dvcn  19845  evlsval2  19979  deg1mul3le  20077  deg1tmle  20078  dvdsq1p  20121  ig1peu  20132  ig1pdvds  20137  ply1term  20161  coeid3  20197  dgrmulc  20227  dvply1  20239  aaliou2  20295  efcvx  20403  tanord  20478  eflogeq  20534  logdivlti  20553  logccv  20592  recxpcl  20604  cxplea  20625  cxpeq  20679  ang180  20694  isosctrlem2  20701  cxp2lim  20853  amgm  20867  muval1  20954  dvdssqf  20959  mumullem2  21001  mumul  21002  bcmono  21099  lgsneg  21141  lgsdilem  21144  lgsdirprm  21151  lgsdir  21152  lgsdi  21154  lgsne0  21155  cyclispthon  21658  vdgrfval  21704  gxcom  21895  gxnn0add  21900  nvmul0or  22171  ipval2lem2  22238  ipval2lem5  22244  lnoadd  22297  lnosub  22298  lnomul  22299  shless  22899  shlej1  22900  kbmul  23496  homco2  23518  kbass2  23658  eliccelico  24175  elicoelioo  24176  iocinioc2  24177  iocinif  24179  difioo  24180  xrge0adddir  24250  xrge0npcan  24251  isarchi2  24290  rhmdvdsr  24291  pstmfval  24326  fmcncfil  24352  zrhnm  24388  qqhnm  24409  volfiniune  24621  dya2iocnrect  24666  probinc  24714  cndprob01  24728  cvmsss2  24996  cvmlift2lem10  25034  binomrisefac  25393  br6  25415  funsseq  25428  frrlem4  25620  brbtwn2  25879  colinearalglem1  25880  colinearalg  25884  axcgrtr  25889  axsegconlem8  25898  axsegconlem9  25899  axsegconlem10  25900  axcontlem2  25939  axcontlem10  25947  cgrtriv  25971  5segofs  25975  btwnouttr2  25991  btwnxfr  26025  lineext  26045  btwnconn1lem13  26068  brsegle2  26078  nn0prpwlem  26367  finlocfin  26421  comppfsc  26429  blbnd  26538  ismtyima  26554  rrndstprj2  26582  ghomdiv  26601  grpokerinj  26602  ofmpteq  26888  diophrw  26929  eldioph2lem1  26930  diophrex  26946  rencldnfi  26994  pellexlem2  27005  pellqrexplicit  27052  infmrgelbi  27053  pellfundglb  27060  pellfund14gap  27062  rmxycomplete  27092  congadd  27143  acongeq  27160  jm2.19  27176  jm2.23  27179  jm2.20nn  27180  jm2.27  27191  jm3.1  27203  lnmepi  27272  lmhmlnmsplit  27274  pwssplit1  27277  pwssplit2  27278  pwssplit3  27279  uvcresum  27331  frlmsslsp  27337  frlmup4  27342  enfixsn  27346  lindff1  27379  f1lindf  27381  lsslindf  27389  islindf4  27397  hbtlem2  27417  dgraa0p  27443  psgnunilem4  27509  idomrootle  27600  hashgcdlem  27605  proot1hash  27608  rfcnnnub  27795  climsuse  27822  stoweidlem17  27854  stoweidlem19  27856  stoweidlem20  27857  stoweidlem22  27859  stoweidlem28  27865  stoweidlem34  27871  stoweidlem44  27881  stoweidlem60  27897  wallispilem3  27904  fzoopth  28260  modaddmulmod  28279  swrdnd  28314  swrdvalodmlem1  28319  swrdccatin12lem3a  28340  nbhashuvtx1  28529  usgreghash2spot  28630  bnj517  29430  lubunNEW  29945  lsatfixedN  29981  lssat  29988  lshpkrlem4  30085  op0cl  30156  cvrcon3b  30249  atlen0  30282  atcvreq0  30286  atnle  30289  atlatmstc  30291  atlatle  30292  cvlcvr1  30311  hlsupr2  30358  hlrelat2  30374  cvrexchlem  30390  lnnat  30398  atcvrj2b  30403  3dimlem3  30432  3dim1  30438  1cvrjat  30446  llni  30479  llni2  30483  llnexatN  30492  2llnmat  30495  lplni  30503  2atnelpln  30515  llncvrlpln2  30528  2llnmj  30531  lplnexatN  30534  lplnexllnN  30535  2llnm3N  30540  lvoli  30546  lvoli3  30548  lvolnle3at  30553  islvol2aN  30563  4atlem4a  30570  4atlem4b  30571  4atlem11  30580  lplncvrlvol2  30586  2lplnmj  30593  islinei  30711  linepmap  30746  lnjatN  30751  lncvrat  30753  lncmp  30754  elpaddn0  30771  elpaddatriN  30774  elpaddat  30775  paddcom  30784  paddss2  30789  paddss12  30790  paddasslem4  30794  paddasslem9  30799  paddasslem10  30800  pmodl42N  30822  pmapjoin  30823  llnmod1i2  30831  polcon2bN  30891  pclfinclN  30921  poml4N  30924  poml6N  30926  osumcllem1N  30927  osumcllem2N  30928  osumcllem11N  30937  osumclN  30938  pmapojoinN  30939  pexmidlem2N  30942  pexmidlem3N  30943  pexmidlem4N  30944  pexmidlem6N  30946  pexmidlem7N  30947  pl42lem2N  30951  pl42lem3N  30952  pl42lem4N  30953  pl42N  30954  lhprelat3N  31011  4atex  31047  lauteq  31066  lautco  31068  ltrncoidN  31099  ltrneq2  31119  ltrnideq  31146  trlnle  31157  trlval3  31158  cdlemc  31168  cdlemd9  31177  cdlemd  31178  cdleme21j  31307  cdleme21  31308  cdleme29ex  31345  cdlemefr27cl  31374  cdlemefs27cl  31384  cdleme32d  31415  cdleme32f  31417  cdleme35h2  31428  cdleme40m  31438  cdleme17d3  31467  cdleme48fvg  31471  cdlemeg46fvcl  31477  cdlemeg46fgN  31505  cdleme48fgv  31509  cdleme50trn3  31524  cdlemb3  31577  cdlemg8  31602  cdlemg11a  31608  cdlemg15a  31626  cdlemg15  31627  cdlemg16  31628  cdlemg16z  31630  cdlemg17dN  31634  cdlemg24  31659  cdlemg37  31660  cdlemg29  31676  cdlemg33b  31678  cdlemg38  31686  cdlemg40  31688  trlco  31698  cdlemg44b  31703  ltrncom  31709  trljco  31711  tendococl  31743  tendoplcl  31752  tendoplcom  31753  cdlemj2  31793  tendoid0  31796  tendo1ne0  31799  cdlemk25-3  31875  cdlemk36  31884  cdlemkid4  31905  cdlemk19x  31914  cdlemk53  31928  cdlemk56  31942  cdleml5N  31951  tendospcanN  31995  cdlemm10N  32090  dihord6apre  32228  dihord  32236  dihmeetlem1N  32262  dihglblem2N  32266  dihmeetlem2N  32271  dihmeetbN  32275  dihmeetlem5  32280  dihmeetlem6  32281  dihmeetlem7N  32282  dihmeetlem10N  32288  dihmeetlem12N  32290  dihmeetlem16N  32294  dihmeetlem17N  32295  dihmeetlem18N  32296  dihmeetALTN  32299  dihlspsnssN  32304  dvh3dim2  32420  dvh3dim3N  32421  lcfrlem16  32530  mapdrvallem2  32617  mapdh8ad  32751  hgmapvvlem3  32900
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator