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

Theorem simpl2 1009
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 1006 . 2  |-  ( (
ph  /\  ps  /\  ch )  ->  ps )
21adantr 466 1  |-  ( ( ( ph  /\  ps  /\ 
ch )  /\  th )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  simpll2  1045  simprl2  1051  simp1l2  1099  simp2l2  1105  simp3l2  1111  3anandirs  1367  rspc3ev  3133  brcogw  4960  f1prex  6136  weniso  6199  ofmpteq  6503  tfisi  6638  mpt2sn  6837  smogt  7036  smorndom  7037  omeulem1  7233  nnmord  7283  nnmword  7284  difsnen  7602  enfixsn  7629  mapunen  7689  ac6sfi  7763  ordiso2  7978  wemaplem2  8010  wemapso  8014  wemapso2lem  8015  en2eqpr  8385  acndom  8428  infmap2  8594  cflim2  8639  cfsmolem  8646  coftr  8649  fin23lem26  8701  isf32lem9  8737  fin1a2lem9  8784  fin1a2lem10  8785  ac6num  8855  gchdomtri  9000  canth4  9018  gchpwdom  9041  gruima  9173  grudomon  9188  prn0  9360  distrlem4pr  9397  prlem934  9404  addcan  9763  addcan2  9764  ltmul1a  10400  supmul1  10522  uzsupss  11202  xaddass  11481  xleadd1a  11485  xlesubadd  11495  xmulass  11519  xlemul2a  11521  xadddilem  11526  xadddi  11527  ixxdisj  11596  ixxun  11597  ixxlb  11603  ixxlbOLD  11604  icoshftf1o  11701  icodisj  11703  lincmb01cmp  11721  iccf1o  11722  ssfzoulel  11950  modaddmulmod  12101  ltexp2a  12269  leexp2  12272  ltexp2r  12274  exple1  12277  expnlbnd2  12348  ccatass  12675  ccatopth  12767  swrdccatin12lem2a  12782  repswccat  12829  2cshw  12853  repsco  12877  s2f1o  12940  limsupgle  13473  limsupgre  13480  limsupgreOLD  13481  addcn2  13595  mulcn2  13597  binomrisefac  14033  dvdsval2  14246  dvdsadd2b  14285  dvdsmod  14300  oexpneg  14306  sadass  14383  gcdass  14451  rplpwr  14462  rppwr  14463  lcmass  14517  coprmdvds2  14598  rpmulgcd2  14600  rpexp  14610  rpdvds  14614  coprmprod  14616  prmdiveq  14672  odzdvds  14678  odzdvdsOLD  14684  coprimeprodsq2  14698  pythagtriplem3  14706  pythagtriplem4  14707  pcdvdsb  14756  vdwnnlem1  14883  0ram  14916  ramz2  14920  ramub1lem1  14922  mremre  15448  mrieqv2d  15483  lubss  16305  lubun  16307  clatleglb  16310  clatglbss  16311  mrelatglb  16368  isnsgrp  16469  issubmnd  16502  gsumccat  16563  frmdss2  16585  nmzsubg  16796  ghmnsgima  16844  gsmsymgreqlem1  17009  psgnunilem4  17076  odmodnn0  17127  odnncl  17132  odmod  17133  oddvds  17134  odeq  17137  odmulgid  17143  odmulgeq  17146  odbezout  17147  odf1o1  17159  odf1o2  17160  odngen  17164  gexdvdsi  17172  pgpfi1  17185  odcau  17194  subgslw  17206  fislw  17215  lsmless1x  17234  lsmless2x  17235  lsmsubm  17243  lsmmod  17263  lsmmod2  17264  efgsfo  17327  odadd1  17424  odadd2  17425  odadd  17426  lsmcomx  17432  prdscmnd  17437  gsumconst  17505  srg1zr  17700  csrgbinom  17717  ring1eq0  17758  mulgass2  17767  cntzsubr  17978  isabvd  17986  0lmhm  18201  lmhmvsca  18206  reslmhm2b  18215  pwssplit1  18220  pwssplit2  18221  pwssplit3  18222  lbspss  18243  lspsnat  18306  lidldvgen  18417  issubassa  18486  evlsval2  18681  coe1subfv  18797  coe1sclmul  18813  coe1sclmul2  18815  xrsdsreclblem  18952  cssmre  19193  obs2ss  19229  uvcresum  19288  frlmsslsp  19291  frlmup4  19296  lindff1  19315  f1lindf  19317  lsslindf  19325  islindf4  19333  mpt2matmul  19408  mamutpos  19420  scmatscmide  19469  mavmulsolcl  19513  mulmarep1gsum2  19536  mdetdiaglem  19560  mdetdiag  19561  mdetunilem1  19574  mdetunilem3  19576  mdetunilem9  19582  maducoeval2  19602  madurid  19606  slesolinvbi  19643  cramerimplem1  19645  cramerlem1  19649  cramer  19653  cpmatel2  19674  m2cpm  19702  m2pmfzmap  19708  m2cpminvid2lem  19715  m2cpminvid2  19716  decpmatmul  19733  pmatcollpw1lem2  19736  pmatcollpw1  19737  pmatcollpw2lem  19738  pmatcollpwfi  19743  pm2mpcl  19758  mply1topmatcl  19766  mp2pm2mplem2  19768  mp2pm2mplem4  19770  mp2pm2mplem5  19771  mp2pm2mp  19772  pm2mpghmlem2  19773  pm2mpghmlem1  19774  chfacfisfcpmat  19816  topssnei  20077  cnconst2  20236  cnpresti  20241  cnprest2  20243  cnpdis  20246  cnt0  20299  cnt1  20303  cnhaus  20307  sscmp  20357  hauscmp  20359  cnconn  20374  uncon  20381  finlocfin  20472  comppfsc  20484  kgen2ss  20507  ptpjopn  20564  prdstopn  20580  ptrescn  20591  qtopss  20667  kqfvima  20682  fbssint  20790  fbasrn  20836  filuni  20837  fmss  20898  rnelfm  20905  fmufil  20911  fmco  20913  flimss2  20924  flimss1  20925  flimrest  20935  cnpflf2  20952  flfcnp  20956  supnfcls  20972  fclsss1  20974  fclsss2  20975  isfcf  20986  subgntr  21058  opnsubg  21059  cldsubg  21062  ghmcnp  21066  ustuqtop1  21193  bldisj  21350  blgt0  21351  bl2in  21352  blss2ps  21355  blss2  21356  blssps  21376  blss  21377  xmetresbl  21389  lpbl  21455  blcld  21457  stdbdmopn  21470  metcnp3  21492  metcnp  21493  metcnp2  21494  txmetcnp  21499  blval2  21514  nmoix  21671  nmoi2  21672  nmoixOLD  21687  nmoi2OLD  21688  nmotri  21697  metdsge  21803  metdseq0  21808  metdsgeOLD  21818  metdseq0OLD  21823  iocopnst  21905  xrhmeo  21911  nmhmcn  22071  cphsqrtcl2  22101  cphsqrtcl3  22102  pjth  22330  ovoliunlem2  22393  volun  22435  mbfimaopn2  22550  iblconst  22712  limcvallem  22763  dvfval  22789  dvcnp2  22811  dvcn  22812  deg1mul3le  23002  deg1tmle  23003  dvdsq1p  23048  ig1peu  23059  ig1peuOLD  23060  ig1pdvds  23065  ig1pdvdsOLD  23071  ply1term  23095  coeid3  23131  dgrmulc  23162  dvply1  23174  aaliou2  23233  efcvx  23341  tanord  23424  eflogeq  23488  logdivlti  23506  logccv  23545  recxpcl  23557  cxplea  23578  cxpeq  23634  ang180  23680  isosctrlem2  23685  cxp2lim  23839  amgm  23853  muval1  23997  dvdssqf  24002  mumullem2  24044  mumul  24045  bcmono  24142  lgsneg  24184  lgsdilem  24187  lgsdirprm  24194  lgsdir  24195  lgsdi  24197  lgsne0  24198  brbtwn2  24872  colinearalglem1  24873  colinearalg  24877  axcgrtr  24882  axsegconlem8  24891  axsegconlem9  24892  axsegconlem10  24893  axcontlem2  24932  axcontlem10  24940  cyclispthon  25298  wwlknext  25389  clwlkisclwwlklem0  25453  erclwwlksym  25479  eleclclwwlknlem2  25483  erclwwlkneqlen  25489  erclwwlknsym  25491  vdgrfval  25560  nbhashuvtx1  25580  usgreghash2spot  25734  extwwlkfablem2  25743  numclwwlk3lem  25773  frgraregord13  25784  gxcom  25934  gxnn0add  25939  nvmul0or  26210  ipval2lem2  26277  ipval2lem5  26283  lnoadd  26336  lnosub  26337  lnomul  26338  shless  26949  shlej1  26950  kbmul  27545  homco2  27567  kbass2  27707  eliccelico  28304  elicoelioo  28305  iocinioc2  28306  iocinif  28308  difioo  28309  xrge0adddir  28401  xrge0npcan  28403  isarchi2  28448  archiabl  28461  rhmdvdsr  28528  pstmfval  28646  fmcncfil  28684  zrhnm  28720  qqhnm  28741  nexple  28778  volfiniune  29000  dya2iocnrect  29050  probinc  29201  cndprob01  29215  signswmnd  29393  bnj517  29643  cvmsss2  29944  cvmlift2lem10  29982  br6  30343  funsseq  30355  frrlem4  30463  cgrtriv  30713  5segofs  30717  btwnouttr2  30733  btwnxfr  30767  lineext  30787  btwnconn1lem13  30810  brsegle2  30820  nn0prpwlem  30922  blbnd  32026  ismtyima  32042  rrndstprj2  32070  ghomdiv  32089  grpokerinj  32090  lsatfixedN  32487  lssat  32494  lshpkrlem4  32591  cvrcon3b  32755  atlen0  32788  atcvreq0  32792  atnle  32795  atlatmstc  32797  atlatle  32798  cvlcvr1  32817  hlsupr2  32864  hlrelat2  32880  cvrexchlem  32896  lnnat  32904  atcvrj2b  32909  3dimlem3  32938  3dim1  32944  1cvrjat  32952  llni  32985  llni2  32989  llnexatN  32998  2llnmat  33001  lplni  33009  2atnelpln  33021  llncvrlpln2  33034  2llnmj  33037  lplnexatN  33040  lplnexllnN  33041  2llnm3N  33046  lvoli  33052  lvoli3  33054  lvolnle3at  33059  islvol2aN  33069  4atlem4a  33076  4atlem4b  33077  4atlem11  33086  lplncvrlvol2  33092  2lplnmj  33099  islinei  33217  linepmap  33252  lnjatN  33257  lncvrat  33259  lncmp  33260  elpaddn0  33277  elpaddatriN  33280  elpaddat  33281  paddcom  33290  paddss2  33295  paddss12  33296  paddasslem4  33300  paddasslem9  33305  paddasslem10  33306  pmodl42N  33328  pmapjoin  33329  llnmod1i2  33337  polcon2bN  33397  pclfinclN  33427  poml4N  33430  poml6N  33432  osumcllem1N  33433  osumcllem2N  33434  osumcllem11N  33443  osumclN  33444  pmapojoinN  33445  pexmidlem2N  33448  pexmidlem3N  33449  pexmidlem4N  33450  pexmidlem6N  33452  pexmidlem7N  33453  pl42lem2N  33457  pl42lem3N  33458  pl42lem4N  33459  pl42N  33460  lhprelat3N  33517  4atex  33553  lauteq  33572  lautco  33574  ltrncoidN  33605  ltrneq2  33625  ltrnideq  33653  trlnle  33664  trlval3  33665  cdlemc  33675  cdlemd9  33684  cdlemd  33685  cdleme21j  33815  cdleme21  33816  cdleme29ex  33853  cdlemefr27cl  33882  cdlemefs27cl  33892  cdleme32d  33923  cdleme32f  33925  cdleme35h2  33936  cdleme40m  33946  cdleme17d3  33975  cdleme48fvg  33979  cdlemeg46fvcl  33985  cdlemeg46fgN  34013  cdleme48fgv  34017  cdleme50trn3  34032  cdlemb3  34085  cdlemg8  34110  cdlemg11a  34116  cdlemg15a  34134  cdlemg15  34135  cdlemg16  34136  cdlemg16z  34138  cdlemg17dN  34142  cdlemg24  34167  cdlemg37  34168  cdlemg29  34184  cdlemg33b  34186  cdlemg38  34194  cdlemg40  34196  trlco  34206  cdlemg44b  34211  ltrncom  34217  trljco  34219  tendococl  34251  tendoplcl  34260  tendoplcom  34261  cdlemj2  34301  tendoid0  34304  tendo1ne0  34307  cdlemk25-3  34383  cdlemk36  34392  cdlemkid4  34413  cdlemk19x  34422  cdlemk53  34436  cdlemk56  34450  cdleml5N  34459  tendospcanN  34503  cdlemm10N  34598  dihord6apre  34736  dihord  34744  dihmeetlem1N  34770  dihglblem2N  34774  dihmeetlem2N  34779  dihmeetbN  34783  dihmeetlem5  34788  dihmeetlem6  34789  dihmeetlem7N  34790  dihmeetlem10N  34796  dihmeetlem12N  34798  dihmeetlem16N  34802  dihmeetlem17N  34803  dihmeetlem18N  34804  dihmeetALTN  34807  dihlspsnssN  34812  dvh3dim2  34928  dvh3dim3N  34929  lcfrlem16  35038  mapdrvallem2  35125  mapdh8ad  35259  hgmapvvlem3  35408  diophrw  35513  eldioph2lem1  35514  diophrex  35530  rencldnfi  35576  pellexlem2  35587  pellqrexplicit  35636  infmrgelbi  35637  infmrgelbiOLD  35638  pellfundglb  35646  pellfund14gap  35648  rmxycomplete  35678  congadd  35729  acongeq  35746  jm2.19  35761  jm2.23  35764  jm2.20nn  35765  jm2.27  35776  jm3.1  35788  lnmepi  35856  lmhmlnmsplit  35858  hbtlem2  35896  dgraa0p  35928  idomrootle  35982  hashgcdlem  35987  proot1hash  35990  iocunico  36008  iocinico  36009  relexpxpmin  36222  rfcnnnub  37273  uzwo4  37308  supxrge  37458  snunioo2  37498  iccintsng  37516  climsuse  37570  lptre2pt  37603  limcleqr  37608  0ellimcdiv  37613  dvnprodlem1  37704  volioc  37732  stoweidlem17  37760  stoweidlem19  37762  stoweidlem20  37763  stoweidlem22  37765  stoweidlem28  37771  stoweidlem34  37778  stoweidlem44  37788  stoweidlem60  37804  wallispilem3  37812  fourierdlem42  37895  fourierdlem42OLD  37896  fourierdlem48  37901  fourierdlem51  37904  fourierdlem54  37907  fourierdlem74  37927  fourierdlem77  37930  fourierdlem87  37940  fourierdlem97  37950  ovnsubaddlem2  38240  fzopredsuc  38533  oexpnegALTV  38619  oexpnegnz  38620  tgblthelfgott  38721  repswpfx  38790  fun2dmnop  38833  eluzge0nn0  38850  fzoopth  38860  rmsupp0  39746  rmsuppss  39748  lincresunit3lem3  39860  lincresunit3lem2  39866  lindssnlvec  39872  fdivmptf  39945  refdivmptf  39946  elbigolo1  39961
  Copyright terms: Public domain W3C validator