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

Theorem simpr2 988
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.)
Assertion
Ref Expression
simpr2  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )

Proof of Theorem simpr2
StepHypRef Expression
1 simp2 982 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  ch )
21adantl 463 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 958
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 960
This theorem is referenced by:  simplr2  1024  simprr2  1030  simp1r2  1078  simp2r2  1084  simp3r2  1090  3anandis  1313  wereu  4703  isopolem  6023  fr3nr  6380  frfi  7545  intrnfi  7654  fisupcl  7705  cnfcomlem  7920  cnfcomlemOLD  7928  ackbij1lem15  8391  cofsmo  8426  sornom  8434  fpwwe2lem5  8788  dedekindle  9521  supmul1  10282  uzletr  10856  xlesubadd  11213  elioc2  11345  elico2  11346  elicc2  11347  fz0fzelfz0  11472  fseq1p1m1  11517  swrdsymbeq  12324  ccatswrd  12333  swrdswrdlem  12336  tanadd  13433  dvds2ln  13545  cshwsidrepsw  14102  ressress  14217  f1ovscpbl  14446  mreexexlem4d  14567  mreexexd  14568  iscatd2  14601  2oppccomf  14646  issubc3  14741  fthmon  14819  fuccocl  14856  fucidcl  14857  invfuc  14866  curf2cl  15023  yonedalem4c  15069  yonedalem3  15072  pospo  15125  latjle12  15214  latjlej1  15217  latnlej2  15223  latlem12  15230  latmlem1  15233  latledi  15241  latjass  15247  latj12  15248  latj32  15249  latj13  15250  latj31  15251  latjrot  15252  latjjdi  15255  latjjdir  15256  latdisdlem  15341  prdsmndd  15436  frmdmnd  15516  grpsubrcan  15586  grpsubadd  15592  grpaddsubass  15594  grpsubsub4  15597  grppnpcan2  15598  grpnpncan  15599  mulgnndir  15628  mulgnn0dir  15629  mulgdir  15631  mulgnnass  15634  mulgnn0ass  15635  mulgass  15636  mulgsubdir  15637  pwsmulg  15648  issubg2  15675  eqgval  15709  divsgrp  15715  galcan  15801  gacan  15802  oppgmnd  15848  symggrp  15884  fvcosymgeq  15913  pmtrprfv  15938  psgnunilem3  15981  cmn32  16274  cmn12  16276  abladdsub  16283  mulgdi  16293  mulgsubdi  16296  dprdss  16499  dprdz  16500  dprdf1o  16502  dprdsn  16506  dprd2da  16514  dmdprdsplit  16519  ablfac1b  16544  pgpfac1lem5  16553  rngi  16592  prdsrngd  16638  opprrng  16656  mulgass3  16662  dvrass  16715  subrgunit  16806  issubrg2  16808  abvdiv  16845  lsssn0  16950  islss3  16961  prdslmodd  16971  islmhm2  17040  lspsolv  17145  islbs2  17156  islbs3  17157  lbsextlem4  17163  sralmod  17189  issubassa  17316  sraassa  17317  psrbaglesupp  17368  psrbaglesuppOLD  17369  psrbaglecl  17370  psrbagcon  17373  psrgrp  17402  psrlmod  17405  psrrng  17416  psrassa  17419  psgndiflemB  17871  ipdir  17909  ipdi  17910  ipsubdir  17912  ipsubdi  17913  ipass  17915  ipassr  17916  ipassr2  17917  isphld  17924  ocvlss  17938  mamudm  18129  matrng  18171  matassa  18172  ofco2  18173  ma1repveval  18223  mdetunilem1  18259  mdetunilem9  18267  iinopn  18356  restopnb  18620  subbascn  18699  nrmsep2  18801  isnrm3  18804  regsep2  18821  dnsconst  18823  dfcon2  18864  1stcelcls  18906  dislly  18942  ptuni2  18990  tx1stc  19064  0nelfb  19245  infil  19277  fsubbas  19281  filssufilg  19325  hauspwpwf1  19401  cnextcn  19480  tmdcn2  19501  ustuqtoplem  19655  utopsnneiplem  19663  psmettri  19728  isxmet2d  19743  xmettri  19767  xmetres2  19777  bldisj  19814  blss2ps  19819  blss2  19820  xmstri2  19882  mstri2  19883  xmstri  19884  mstri  19885  xmstri3  19886  mstri3  19887  msrtri  19888  comet  19929  stdbdbl  19933  met2ndci  19938  ngprcan  20042  ngplcan  20043  ngpsubcan  20046  nrgdsdi  20087  nrgdsdir  20088  nlmdsdi  20103  nlmdsdir  20104  blcvx  20216  icoopnst  20352  pi1grplem  20462  cvsdiv  20522  cvsdivcl  20523  cphdivcl  20542  cphsubdir  20567  cphsubdi  20568  tchcph  20593  bcthlem5  20680  volfiniun  20869  volcn  20927  itg1val2  21003  dvconst  21232  dvlip  21306  ftc1a  21350  ulmval  21729  ulmdvlem3  21751  ang180  22094  cvxcl  22262  scvxcvx  22263  sgmmul  22424  dchrabl  22477  f1otrge  22940  xmstrkgc  22954  colinearalglem1  22974  axcgrtr  22983  axeuclidlem  23030  axcontlem3  23034  axcontlem4  23035  axcontlem7  23038  eengtrkg  23053  eengtrkge  23054  isspthonpth  23305  wlkdvspth  23329  iseupa  23408  grpomuldivass  23558  grponpncan  23564  grpodiveq  23565  ablomuldiv  23598  ablodivdiv4  23600  ablonnncan1  23604  nvmdi  23852  nvsubadd  23857  dipassr  24068  archiabllem2c  26035  srgi  26046  dvrdir  26110  dvrcan5  26113  reofld  26161  pstmfval  26176  qqhval2lem  26263  qqhvq  26269  measdivcstOLD  26491  measdivcst  26492  erdszelem9  26934  rescon  26982  cvmseu  27012  cvmlift2lem10  27048  cvmlift2lem12  27050  frrlem4  27617  cgrid2  27880  segconeu  27888  btwncomim  27890  btwnswapid  27894  trisegint  27905  cgrxfr  27932  brofs2  27954  endofsegid  27962  btwnconn2  27979  seglemin  27990  segletr  27991  btwnsegle  27994  colinbtwnle  27995  broutsideof2  27999  btwnoutside  28002  broutsideof3  28003  outsideoftr  28006  outsidele  28009  fvray  28018  fvline  28021  ellines  28029  ftc1anc  28316  sdclem1  28480  sstotbnd2  28514  iscringd  28640  irrapxlem6  29010  jm2.26lem3  29192  dgrsub2  29333  mpaaroot  29354  mendrng  29391  mendlmod  29392  mendassa  29393  rfcnpre3  29597  fmuldfeq  29606  stoweidlem43  29681  stoweidlem52  29690  stoweidlem53  29691  stoweidlem56  29694  stoweidlem57  29695  stoweidlem60  29698  uzuzle  30033  el2spthonot0  30233  usg2wotspth  30246  2spontn0vne  30249  ltsubsubaddltsub  30310  clwlkfoclwwlk  30361  rusgranumwlks  30417  rusgranumwwlkg  30420  3vfriswmgra  30440  frgrareggt1  30552  ldepsprlem  30712  lincresunit3  30721  lincreslvec3  30722  bnj1098  31476  bnj149  31567  bnj1118  31674  lsmsat  32223  lfladdcl  32286  lflnegcl  32290  lflvscl  32292  eqlkr  32314  lshpkrlem4  32328  lshpkrlem6  32330  ldualgrplem  32360  lduallmodlem  32367  latmassOLD  32444  latm12  32445  latm32  32446  latmrot  32447  latmmdiN  32449  latmmdir  32450  omlfh1N  32473  omlfh3N  32474  cvrnbtwn2  32490  cvlexchb1  32545  cvlsupr2  32558  hlatjass  32584  hlatj12  32585  hlatj32  32586  cvrat  32636  cvrat2  32643  atltcvr  32649  atexchltN  32655  cvrat3  32656  cvrat4  32657  atbtwnexOLDN  32661  atbtwnex  32662  3dimlem3  32675  3dimlem3OLDN  32676  3at  32704  2atneat  32729  llncmp  32736  2at0mat0  32739  2atmat0  32740  llncvrlpln  32772  lplncmp  32776  2llnjaN  32780  4atlem11  32823  lplncvrlvol  32830  lvolcmp  32831  2atm2atN  32999  elpaddatriN  33017  paddasslem8  33041  paddass  33052  padd12N  33053  paddssw2  33058  paddss  33059  pmod1i  33062  pmodN  33064  pmapjlln1  33069  atmod1i1  33071  atmod1i2  33073  pexmidlem2N  33185  pl42lem2N  33194  pl42lem3N  33195  pl42lem4N  33196  pl42N  33197  lhpm0atN  33243  lautlt  33305  lautcvr  33306  lautj  33307  lautm  33308  ltrneq2  33362  cdlemd1  33412  cdleme1b  33440  cdleme1  33441  cdleme2  33442  cdleme3e  33446  cdlemefr27cl  33617  cdlemefs27cl  33627  cdleme42ke  33699  cdleme42mN  33701  cdlemf2  33776  cdlemftr2  33780  trljco  33954  tgrpgrplem  33963  tendoplass  33997  tendodi1  33998  tendodi2  33999  cdlemk34  34124  cdlemk36  34127  erngdvlem3-rN  34212  tendospdi1  34235  dialss  34261  dvhvaddass  34312  dvhopvsca  34317  dvhlveclem  34323  diblss  34385  diclss  34408  diclspsn  34409  cdlemn11pre  34425  dihmeetlem12N  34533  dihmeetlem16N  34537  dihmeetlem17N  34538  dihmeetlem18N  34539  dvh4dimN  34662  lpolconN  34702  dochpolN  34705  lclkr  34748  lclkrs  34754  lcfr  34800
  Copyright terms: Public domain W3C validator