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  1321  rspc3ev  3078  brcogw  5003  weniso  6040  ofmpteq  6333  tfisi  6464  smogt  6820  smorndom  6821  omeulem1  7013  nnmord  7063  nnmword  7064  difsnen  7385  enfixsn  7412  mapunen  7472  ac6sfi  7548  ordiso2  7721  wemaplem2  7753  wemapso  7757  wemapso2lem  7759  en2eqpr  8166  acndom  8213  infmap2  8379  cflim2  8424  cfsmolem  8431  coftr  8434  fin23lem26  8486  isf32lem9  8522  fin1a2lem9  8569  fin1a2lem10  8570  ac6num  8640  gchdomtri  8788  canth4  8806  gchpwdom  8829  gruima  8961  grudomon  8976  prn0  9150  distrlem4pr  9187  prlem934  9194  addcan  9545  addcan2  9546  ltmul1a  10170  ledivmulOLD  10198  supmul1  10287  uzsupss  10939  xaddass  11204  xleadd1a  11208  xlesubadd  11218  xmulass  11242  xlemul2a  11244  xadddilem  11249  xadddi  11250  ixxdisj  11307  ixxun  11308  ixxlb  11314  icoshftf1o  11400  icodisj  11402  lincmb01cmp  11420  iccf1o  11421  ssfzoulel  11613  modaddmulmod  11757  ltexp2a  11907  leexp2  11910  ltexp2r  11912  exple1  11915  expnlbnd2  11987  ccatass  12278  swrdnd  12318  ccatopth  12356  swrdccatin12lem2a  12368  repswccat  12415  2cshw  12439  repsco  12459  s2f1o  12518  limsupgle  12947  limsupgre  12951  addcn2  13063  mulcn2  13065  dvdsval2  13530  dvdsadd2b  13567  dvdsmod  13582  oexpneg  13587  sadass  13659  gcdass  13721  rplpwr  13732  rppwr  13733  coprmdvds2  13781  rpmulgcd2  13783  rpexp  13798  rpdvds  13802  prmdiveq  13853  odzdvds  13859  coprimeprodsq2  13869  pythagtriplem3  13877  pythagtriplem4  13878  pcdvdsb  13927  vdwnnlem1  14048  0ram  14073  ramz2  14077  ramub1lem1  14079  mremre  14534  mrieqv2d  14569  lubss  15283  lubun  15285  clatleglb  15288  clatglbss  15289  mrelatglb  15346  issubmnd  15441  gsumccat  15510  frmdss2  15532  nmzsubg  15713  ghmnsgima  15761  gsmsymgreqlem1  15926  psgnunilem4  15994  odmodnn0  16034  odnncl  16039  odmod  16040  oddvds  16041  odeq  16044  odmulgid  16046  odmulgeq  16049  odbezout  16050  odf1o1  16062  odf1o2  16063  odngen  16067  gexdvdsi  16073  pgpfi1  16085  odcau  16094  subgslw  16106  fislw  16115  lsmless1x  16134  lsmless2x  16135  lsmsubm  16143  lsmmod  16163  lsmmod2  16164  efgsfo  16227  odadd1  16321  odadd2  16322  odadd  16323  lsmcomx  16329  prdscmnd  16334  gsumconst  16417  csrgbinom  16632  rng1eq0  16672  mulgass2  16680  cntzsubr  16875  isabvd  16883  0lmhm  17098  lmhmvsca  17103  reslmhm2b  17112  pwssplit1  17117  pwssplit2  17118  pwssplit3  17119  lbspss  17140  lspsnat  17203  lidldvgen  17314  issubassa  17372  evlsval2  17581  coe1subfv  17695  coe1sclmul  17710  coe1sclmul2  17712  xrsdsreclblem  17834  cssmre  18093  obs2ss  18129  uvcresum  18193  frlmsslsp  18198  frlmsslspOLD  18199  frlmup4  18204  lindff1  18224  f1lindf  18226  lsslindf  18234  islindf4  18242  mamutpos  18318  mavmulsolcl  18337  mdetunilem1  18393  mdetunilem3  18395  mdetunilem9  18401  maducoeval2  18421  madurid  18425  slesolinvbi  18462  cramerimplem1  18464  cramerlem1  18468  cramer  18472  topssnei  18703  cnconst2  18862  cnpresti  18867  cnprest2  18869  cnpdis  18872  cnt0  18925  cnt1  18929  cnhaus  18933  sscmp  18983  hauscmp  18985  cnconn  19001  uncon  19008  kgen2ss  19103  ptpjopn  19160  prdstopn  19176  ptrescn  19187  qtopss  19263  kqfvima  19278  fbssint  19386  fbasrn  19432  filuni  19433  fmss  19494  rnelfm  19501  fmufil  19507  fmco  19509  flimss2  19520  flimss1  19521  flimrest  19531  cnpflf2  19548  flfcnp  19552  supnfcls  19568  fclsss1  19570  fclsss2  19571  isfcf  19582  subgntr  19652  opnsubg  19653  cldsubg  19656  ghmcnp  19660  ustuqtop1  19791  bldisj  19948  blgt0  19949  bl2in  19950  blss2ps  19953  blss2  19954  blssps  19974  blss  19975  xmetresbl  19987  lpbl  20053  blcld  20055  stdbdmopn  20068  metcnp3  20090  metcnp  20091  metcnp2  20092  txmetcnp  20097  blval2  20125  nmoix  20283  nmoi2  20284  nmotri  20293  metdsge  20400  metdseq0  20405  iocopnst  20487  xrhmeo  20493  nmhmcn  20650  cphsqrcl2  20680  cphsqrcl3  20681  pjth  20901  ovoliunlem2  20961  volun  21001  mbfimaopn2  21110  iblconst  21270  limcvallem  21321  dvfval  21347  dvcnp2  21369  dvcn  21370  deg1mul3le  21563  deg1tmle  21564  dvdsq1p  21607  ig1peu  21618  ig1pdvds  21623  ply1term  21647  coeid3  21683  dgrmulc  21713  dvply1  21725  aaliou2  21781  efcvx  21889  tanord  21969  eflogeq  22025  logdivlti  22044  logccv  22083  recxpcl  22095  cxplea  22116  cxpeq  22170  ang180  22185  isosctrlem2  22192  cxp2lim  22345  amgm  22359  muval1  22446  dvdssqf  22451  mumullem2  22493  mumul  22494  bcmono  22591  lgsneg  22633  lgsdilem  22636  lgsdirprm  22643  lgsdir  22644  lgsdi  22646  lgsne0  22647  brbtwn2  23102  colinearalglem1  23103  colinearalg  23107  axcgrtr  23112  axsegconlem8  23121  axsegconlem9  23122  axsegconlem10  23123  axcontlem2  23162  axcontlem10  23170  cyclispthon  23470  vdgrfval  23516  gxcom  23707  gxnn0add  23712  nvmul0or  23983  ipval2lem2  24050  ipval2lem5  24056  lnoadd  24109  lnosub  24110  lnomul  24111  shless  24713  shlej1  24714  kbmul  25310  homco2  25332  kbass2  25472  eliccelico  26018  elicoelioo  26019  iocinioc2  26020  iocinif  26022  difioo  26023  xrge0adddir  26106  xrge0npcan  26108  isarchi2  26153  archiabl  26166  rhmdvdsr  26237  pstmfval  26275  fmcncfil  26313  zrhnm  26350  qqhnm  26371  nexple  26400  volfiniune  26598  dya2iocnrect  26648  probinc  26756  cndprob01  26770  signswmnd  26910  cvmsss2  27115  cvmlift2lem10  27153  binomrisefac  27496  br6  27518  funsseq  27531  frrlem4  27722  cgrtriv  27984  5segofs  27988  btwnouttr2  28004  btwnxfr  28038  lineext  28058  btwnconn1lem13  28081  brsegle2  28091  nn0prpwlem  28470  finlocfin  28524  comppfsc  28532  blbnd  28639  ismtyima  28655  rrndstprj2  28683  ghomdiv  28702  grpokerinj  28703  diophrw  29050  eldioph2lem1  29051  diophrex  29067  rencldnfi  29113  pellexlem2  29124  pellqrexplicit  29171  infmrgelbi  29172  pellfundglb  29179  pellfund14gap  29181  rmxycomplete  29211  congadd  29262  acongeq  29279  jm2.19  29295  jm2.23  29298  jm2.20nn  29299  jm2.27  29310  jm3.1  29322  lnmepi  29391  lmhmlnmsplit  29393  hbtlem2  29433  dgraa0p  29459  idomrootle  29513  hashgcdlem  29518  proot1hash  29521  iocunico  29539  iocinico  29540  rfcnnnub  29711  climsuse  29734  stoweidlem17  29765  stoweidlem19  29767  stoweidlem20  29768  stoweidlem22  29770  stoweidlem28  29776  stoweidlem34  29782  stoweidlem44  29792  stoweidlem60  29808  wallispilem3  29815  eluzge0nn0  30142  fzoopth  30166  wwlknext  30309  clwlkisclwwlklem0  30403  erclwwlksym  30437  eleclclwwlknlem2  30444  erclwwlkneqlen  30451  erclwwlknsym  30453  nbhashuvtx1  30486  usgreghash2spot  30615  extwwlkfablem2  30624  numclwwlk3lem  30654  frgraregord13  30665  mpt2sn  30675  rmsupp0  30732  rmsuppss  30734  pmatcollpw1lem5  30818  pmatcollpw1  30819  mdetdiaglem  30824  mdetdiag  30825  lincresunit3lem3  30897  lincresunit3lem2  30903  lindssnlvec  30909  bnj517  31765  lsatfixedN  32494  lssat  32501  lshpkrlem4  32598  cvrcon3b  32762  atlen0  32795  atcvreq0  32799  atnle  32802  atlatmstc  32804  atlatle  32805  cvlcvr1  32824  hlsupr2  32871  hlrelat2  32887  cvrexchlem  32903  lnnat  32911  atcvrj2b  32916  3dimlem3  32945  3dim1  32951  1cvrjat  32959  llni  32992  llni2  32996  llnexatN  33005  2llnmat  33008  lplni  33016  2atnelpln  33028  llncvrlpln2  33041  2llnmj  33044  lplnexatN  33047  lplnexllnN  33048  2llnm3N  33053  lvoli  33059  lvoli3  33061  lvolnle3at  33066  islvol2aN  33076  4atlem4a  33083  4atlem4b  33084  4atlem11  33093  lplncvrlvol2  33099  2lplnmj  33106  islinei  33224  linepmap  33259  lnjatN  33264  lncvrat  33266  lncmp  33267  elpaddn0  33284  elpaddatriN  33287  elpaddat  33288  paddcom  33297  paddss2  33302  paddss12  33303  paddasslem4  33307  paddasslem9  33312  paddasslem10  33313  pmodl42N  33335  pmapjoin  33336  llnmod1i2  33344  polcon2bN  33404  pclfinclN  33434  poml4N  33437  poml6N  33439  osumcllem1N  33440  osumcllem2N  33441  osumcllem11N  33450  osumclN  33451  pmapojoinN  33452  pexmidlem2N  33455  pexmidlem3N  33456  pexmidlem4N  33457  pexmidlem6N  33459  pexmidlem7N  33460  pl42lem2N  33464  pl42lem3N  33465  pl42lem4N  33466  pl42N  33467  lhprelat3N  33524  4atex  33560  lauteq  33579  lautco  33581  ltrncoidN  33612  ltrneq2  33632  ltrnideq  33659  trlnle  33670  trlval3  33671  cdlemc  33681  cdlemd9  33690  cdlemd  33691  cdleme21j  33820  cdleme21  33821  cdleme29ex  33858  cdlemefr27cl  33887  cdlemefs27cl  33897  cdleme32d  33928  cdleme32f  33930  cdleme35h2  33941  cdleme40m  33951  cdleme17d3  33980  cdleme48fvg  33984  cdlemeg46fvcl  33990  cdlemeg46fgN  34018  cdleme48fgv  34022  cdleme50trn3  34037  cdlemb3  34090  cdlemg8  34115  cdlemg11a  34121  cdlemg15a  34139  cdlemg15  34140  cdlemg16  34141  cdlemg16z  34143  cdlemg17dN  34147  cdlemg24  34172  cdlemg37  34173  cdlemg29  34189  cdlemg33b  34191  cdlemg38  34199  cdlemg40  34201  trlco  34211  cdlemg44b  34216  ltrncom  34222  trljco  34224  tendococl  34256  tendoplcl  34265  tendoplcom  34266  cdlemj2  34306  tendoid0  34309  tendo1ne0  34312  cdlemk25-3  34388  cdlemk36  34397  cdlemkid4  34418  cdlemk19x  34427  cdlemk53  34441  cdlemk56  34455  cdleml5N  34464  tendospcanN  34508  cdlemm10N  34603  dihord6apre  34741  dihord  34749  dihmeetlem1N  34775  dihglblem2N  34779  dihmeetlem2N  34784  dihmeetbN  34788  dihmeetlem5  34793  dihmeetlem6  34794  dihmeetlem7N  34795  dihmeetlem10N  34801  dihmeetlem12N  34803  dihmeetlem16N  34807  dihmeetlem17N  34808  dihmeetlem18N  34809  dihmeetALTN  34812  dihlspsnssN  34817  dvh3dim2  34933  dvh3dim3N  34934  lcfrlem16  35043  mapdrvallem2  35130  mapdh8ad  35264  hgmapvvlem3  35413
  Copyright terms: Public domain W3C validator