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

Theorem simpl2 1000
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 997 . 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 973
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 975
This theorem is referenced by:  simpll2  1036  simprl2  1042  simp1l2  1090  simp2l2  1096  simp3l2  1102  3anandirs  1331  rspc3ev  3227  brcogw  5169  weniso  6236  ofmpteq  6540  tfisi  6671  mpt2sn  6871  smogt  7035  smorndom  7036  omeulem1  7228  nnmord  7278  nnmword  7279  difsnen  7596  enfixsn  7623  mapunen  7683  ac6sfi  7760  ordiso2  7936  wemaplem2  7968  wemapso  7972  wemapso2lem  7974  en2eqpr  8381  acndom  8428  infmap2  8594  cflim2  8639  cfsmolem  8646  coftr  8649  fin23lem26  8701  isf32lem9  8737  fin1a2lem9  8784  fin1a2lem10  8785  ac6num  8855  gchdomtri  9003  canth4  9021  gchpwdom  9044  gruima  9176  grudomon  9191  prn0  9363  distrlem4pr  9400  prlem934  9407  addcan  9759  addcan2  9760  ltmul1a  10387  ledivmulOLD  10415  supmul1  10504  uzsupss  11170  xaddass  11437  xleadd1a  11441  xlesubadd  11451  xmulass  11475  xlemul2a  11477  xadddilem  11482  xadddi  11483  ixxdisj  11540  ixxun  11541  ixxlb  11547  icoshftf1o  11639  icodisj  11641  lincmb01cmp  11659  iccf1o  11660  ssfzoulel  11870  modaddmulmod  12016  ltexp2a  12179  leexp2  12182  ltexp2r  12184  exple1  12187  expnlbnd2  12259  ccatass  12564  swrdnd  12614  ccatopth  12652  swrdccatin12lem2a  12667  repswccat  12714  2cshw  12738  repsco  12762  s2f1o  12821  limsupgle  13256  limsupgre  13260  addcn2  13372  mulcn2  13374  dvdsval2  13843  dvdsadd2b  13880  dvdsmod  13895  oexpneg  13901  sadass  13973  gcdass  14035  rplpwr  14046  rppwr  14047  coprmdvds2  14096  rpmulgcd2  14098  rpexp  14113  rpdvds  14117  prmdiveq  14168  odzdvds  14174  coprimeprodsq2  14186  pythagtriplem3  14194  pythagtriplem4  14195  pcdvdsb  14244  vdwnnlem1  14365  0ram  14390  ramz2  14394  ramub1lem1  14396  mremre  14852  mrieqv2d  14887  lubss  15601  lubun  15603  clatleglb  15606  clatglbss  15607  mrelatglb  15664  issubmnd  15759  gsumccat  15829  frmdss2  15851  nmzsubg  16034  ghmnsgima  16082  gsmsymgreqlem1  16247  psgnunilem4  16315  odmodnn0  16357  odnncl  16362  odmod  16363  oddvds  16364  odeq  16367  odmulgid  16369  odmulgeq  16372  odbezout  16373  odf1o1  16385  odf1o2  16386  odngen  16390  gexdvdsi  16396  pgpfi1  16408  odcau  16417  subgslw  16429  fislw  16438  lsmless1x  16457  lsmless2x  16458  lsmsubm  16466  lsmmod  16486  lsmmod2  16487  efgsfo  16550  odadd1  16644  odadd2  16645  odadd  16646  lsmcomx  16652  prdscmnd  16657  gsumconst  16742  csrgbinom  16982  rng1eq0  17022  mulgass2  17030  cntzsubr  17241  isabvd  17249  0lmhm  17466  lmhmvsca  17471  reslmhm2b  17480  pwssplit1  17485  pwssplit2  17486  pwssplit3  17487  lbspss  17508  lspsnat  17571  lidldvgen  17682  issubassa  17741  evlsval2  17957  coe1subfv  18075  coe1sclmul  18091  coe1sclmul2  18093  xrsdsreclblem  18229  cssmre  18488  obs2ss  18524  uvcresum  18588  frlmsslsp  18593  frlmsslspOLD  18594  frlmup4  18599  lindff1  18619  f1lindf  18621  lsslindf  18629  islindf4  18637  mamutpos  18724  scmatscmide  18773  mavmulsolcl  18817  mdetdiaglem  18864  mdetdiag  18865  mdetunilem1  18878  mdetunilem3  18880  mdetunilem9  18886  maducoeval2  18906  madurid  18910  slesolinvbi  18947  cramerimplem1  18949  cramerlem1  18953  cramer  18957  cpmatel2  18978  m2cpm  19006  m2pmfzmap  19012  m2cpminvid2lem  19019  m2cpminvid2  19020  decpmatmul  19037  pmatcollpw1lem2  19040  pmatcollpw1  19041  pmatcollpw2lem  19042  pmatcollpwfi  19047  pm2mpcl  19062  mply1topmatcl  19070  mp2pm2mplem2  19072  mp2pm2mplem4  19074  mp2pm2mplem5  19075  pm2mpghmlem2  19077  pm2mpghmlem1  19078  chfacfisfcpmat  19120  topssnei  19388  cnconst2  19547  cnpresti  19552  cnprest2  19554  cnpdis  19557  cnt0  19610  cnt1  19614  cnhaus  19618  sscmp  19668  hauscmp  19670  cnconn  19686  uncon  19693  kgen2ss  19788  ptpjopn  19845  prdstopn  19861  ptrescn  19872  qtopss  19948  kqfvima  19963  fbssint  20071  fbasrn  20117  filuni  20118  fmss  20179  rnelfm  20186  fmufil  20192  fmco  20194  flimss2  20205  flimss1  20206  flimrest  20216  cnpflf2  20233  flfcnp  20237  supnfcls  20253  fclsss1  20255  fclsss2  20256  isfcf  20267  subgntr  20337  opnsubg  20338  cldsubg  20341  ghmcnp  20345  ustuqtop1  20476  bldisj  20633  blgt0  20634  bl2in  20635  blss2ps  20638  blss2  20639  blssps  20659  blss  20660  xmetresbl  20672  lpbl  20738  blcld  20740  stdbdmopn  20753  metcnp3  20775  metcnp  20776  metcnp2  20777  txmetcnp  20782  blval2  20810  nmoix  20968  nmoi2  20969  nmotri  20978  metdsge  21085  metdseq0  21090  iocopnst  21172  xrhmeo  21178  nmhmcn  21335  cphsqrtcl2  21365  cphsqrtcl3  21366  pjth  21586  ovoliunlem2  21646  volun  21687  mbfimaopn2  21796  iblconst  21956  limcvallem  22007  dvfval  22033  dvcnp2  22055  dvcn  22056  deg1mul3le  22249  deg1tmle  22250  dvdsq1p  22293  ig1peu  22304  ig1pdvds  22309  ply1term  22333  coeid3  22369  dgrmulc  22399  dvply1  22411  aaliou2  22467  efcvx  22575  tanord  22655  eflogeq  22711  logdivlti  22730  logccv  22769  recxpcl  22781  cxplea  22802  cxpeq  22856  ang180  22871  isosctrlem2  22878  cxp2lim  23031  amgm  23045  muval1  23132  dvdssqf  23137  mumullem2  23179  mumul  23180  bcmono  23277  lgsneg  23319  lgsdilem  23322  lgsdirprm  23329  lgsdir  23330  lgsdi  23332  lgsne0  23333  brbtwn2  23881  colinearalglem1  23882  colinearalg  23886  axcgrtr  23891  axsegconlem8  23900  axsegconlem9  23901  axsegconlem10  23902  axcontlem2  23941  axcontlem10  23949  cyclispthon  24306  wwlknext  24397  clwlkisclwwlklem0  24461  erclwwlksym  24487  eleclclwwlknlem2  24491  erclwwlkneqlen  24497  erclwwlknsym  24499  vdgrfval  24568  nbhashuvtx1  24588  usgreghash2spot  24743  extwwlkfablem2  24752  numclwwlk3lem  24782  frgraregord13  24793  gxcom  24944  gxnn0add  24949  nvmul0or  25220  ipval2lem2  25287  ipval2lem5  25293  lnoadd  25346  lnosub  25347  lnomul  25348  shless  25950  shlej1  25951  kbmul  26547  homco2  26569  kbass2  26709  eliccelico  27253  elicoelioo  27254  iocinioc2  27255  iocinif  27257  difioo  27258  xrge0adddir  27341  xrge0npcan  27343  isarchi2  27388  archiabl  27401  rhmdvdsr  27468  pstmfval  27508  fmcncfil  27546  zrhnm  27583  qqhnm  27604  nexple  27642  volfiniune  27839  dya2iocnrect  27889  probinc  27997  cndprob01  28011  signswmnd  28151  cvmsss2  28356  cvmlift2lem10  28394  binomrisefac  28738  br6  28760  funsseq  28773  frrlem4  28964  cgrtriv  29226  5segofs  29230  btwnouttr2  29246  btwnxfr  29280  lineext  29300  btwnconn1lem13  29323  brsegle2  29333  nn0prpwlem  29715  finlocfin  29769  comppfsc  29777  blbnd  29884  ismtyima  29900  rrndstprj2  29928  ghomdiv  29947  grpokerinj  29948  diophrw  30294  eldioph2lem1  30295  diophrex  30311  rencldnfi  30357  pellexlem2  30368  pellqrexplicit  30415  infmrgelbi  30416  pellfundglb  30423  pellfund14gap  30425  rmxycomplete  30455  congadd  30506  acongeq  30523  jm2.19  30539  jm2.23  30542  jm2.20nn  30543  jm2.27  30554  jm3.1  30566  lnmepi  30635  lmhmlnmsplit  30637  hbtlem2  30677  dgraa0p  30703  idomrootle  30757  hashgcdlem  30762  proot1hash  30765  iocunico  30783  iocinico  30784  lcmass  30818  rfcnnnub  30989  snunioo2  31108  iccintsng  31127  climsuse  31150  lptre2pt  31182  limcleqr  31186  0ellimcdiv  31191  volioc  31290  stoweidlem17  31317  stoweidlem19  31319  stoweidlem20  31320  stoweidlem22  31322  stoweidlem28  31328  stoweidlem34  31334  stoweidlem44  31344  stoweidlem60  31360  wallispilem3  31367  fourierdlem42  31449  fourierdlem48  31455  fourierdlem51  31458  fourierdlem54  31461  fourierdlem74  31481  fourierdlem77  31484  fourierdlem87  31494  fourierdlem97  31504  eluzge0nn0  31798  fzoopth  31809  rmsupp0  32034  rmsuppss  32036  lincresunit3lem3  32148  lincresunit3lem2  32154  lindssnlvec  32160  bnj517  33022  lsatfixedN  33806  lssat  33813  lshpkrlem4  33910  cvrcon3b  34074  atlen0  34107  atcvreq0  34111  atnle  34114  atlatmstc  34116  atlatle  34117  cvlcvr1  34136  hlsupr2  34183  hlrelat2  34199  cvrexchlem  34215  lnnat  34223  atcvrj2b  34228  3dimlem3  34257  3dim1  34263  1cvrjat  34271  llni  34304  llni2  34308  llnexatN  34317  2llnmat  34320  lplni  34328  2atnelpln  34340  llncvrlpln2  34353  2llnmj  34356  lplnexatN  34359  lplnexllnN  34360  2llnm3N  34365  lvoli  34371  lvoli3  34373  lvolnle3at  34378  islvol2aN  34388  4atlem4a  34395  4atlem4b  34396  4atlem11  34405  lplncvrlvol2  34411  2lplnmj  34418  islinei  34536  linepmap  34571  lnjatN  34576  lncvrat  34578  lncmp  34579  elpaddn0  34596  elpaddatriN  34599  elpaddat  34600  paddcom  34609  paddss2  34614  paddss12  34615  paddasslem4  34619  paddasslem9  34624  paddasslem10  34625  pmodl42N  34647  pmapjoin  34648  llnmod1i2  34656  polcon2bN  34716  pclfinclN  34746  poml4N  34749  poml6N  34751  osumcllem1N  34752  osumcllem2N  34753  osumcllem11N  34762  osumclN  34763  pmapojoinN  34764  pexmidlem2N  34767  pexmidlem3N  34768  pexmidlem4N  34769  pexmidlem6N  34771  pexmidlem7N  34772  pl42lem2N  34776  pl42lem3N  34777  pl42lem4N  34778  pl42N  34779  lhprelat3N  34836  4atex  34872  lauteq  34891  lautco  34893  ltrncoidN  34924  ltrneq2  34944  ltrnideq  34971  trlnle  34982  trlval3  34983  cdlemc  34993  cdlemd9  35002  cdlemd  35003  cdleme21j  35132  cdleme21  35133  cdleme29ex  35170  cdlemefr27cl  35199  cdlemefs27cl  35209  cdleme32d  35240  cdleme32f  35242  cdleme35h2  35253  cdleme40m  35263  cdleme17d3  35292  cdleme48fvg  35296  cdlemeg46fvcl  35302  cdlemeg46fgN  35330  cdleme48fgv  35334  cdleme50trn3  35349  cdlemb3  35402  cdlemg8  35427  cdlemg11a  35433  cdlemg15a  35451  cdlemg15  35452  cdlemg16  35453  cdlemg16z  35455  cdlemg17dN  35459  cdlemg24  35484  cdlemg37  35485  cdlemg29  35501  cdlemg33b  35503  cdlemg38  35511  cdlemg40  35513  trlco  35523  cdlemg44b  35528  ltrncom  35534  trljco  35536  tendococl  35568  tendoplcl  35577  tendoplcom  35578  cdlemj2  35618  tendoid0  35621  tendo1ne0  35624  cdlemk25-3  35700  cdlemk36  35709  cdlemkid4  35730  cdlemk19x  35739  cdlemk53  35753  cdlemk56  35767  cdleml5N  35776  tendospcanN  35820  cdlemm10N  35915  dihord6apre  36053  dihord  36061  dihmeetlem1N  36087  dihglblem2N  36091  dihmeetlem2N  36096  dihmeetbN  36100  dihmeetlem5  36105  dihmeetlem6  36106  dihmeetlem7N  36107  dihmeetlem10N  36113  dihmeetlem12N  36115  dihmeetlem16N  36119  dihmeetlem17N  36120  dihmeetlem18N  36121  dihmeetALTN  36124  dihlspsnssN  36129  dvh3dim2  36245  dvh3dim3N  36246  lcfrlem16  36355  mapdrvallem2  36442  mapdh8ad  36576  hgmapvvlem3  36725
  Copyright terms: Public domain W3C validator