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

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

Proof of Theorem simpr3
StepHypRef Expression
1 simp3 983 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 463 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
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:  simplr3  1025  simprr3  1031  simp1r3  1079  simp2r3  1085  simp3r3  1091  3anandis  1313  isopolem  6023  fr3nr  6380  suppfnss  6703  elfir  7653  intrnfi  7654  fisupcl  7705  cnfcomlem  7920  cnfcomlemOLD  7928  ackbij1lem15  8391  pwfseqlem4a  8815  pwfseqlem4  8816  xlesubadd  11213  elioc2  11345  elico2  11346  elicc2  11347  fseq1p1m1  11517  swrdsymbeq  12324  ccatswrd  12333  tanadd  13433  dvds2ln  13545  cshwsidrepsw  14102  ressress  14217  f1ovscpbl  14446  mreexexlem4d  14567  mreexexd  14568  2oppccomf  14646  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  imasmnd2  15440  imasmnd  15441  frmdmnd  15516  grpsubadd  15592  grpaddsubass  15594  grpsubsub4  15597  grppnpcan2  15598  grpnpncan  15599  grpnnncan2  15600  mulgnndir  15628  mulgnn0dir  15629  mulgnnass  15634  mulgnn0ass  15635  mulgass  15636  pwsmulg  15648  imasgrp2  15649  imasgrp  15650  issubg2  15675  divsgrp  15715  galcan  15801  gacan  15802  oppgmnd  15848  symggrp  15884  pmtrprfv  15938  pmtr3ncom  15960  psgnunilem3  15981  frgp0  16236  cmn32  16274  cmn12  16276  abladdsub  16283  mulgdi  16293  mulgsubdi  16296  dprdss  16499  dprdf1o  16502  dprdsn  16506  dmdprdsplit  16519  pgpfac1lem5  16553  rngi  16592  prdsrngd  16638  imasrng  16645  opprrng  16656  mulgass3  16662  dvrass  16715  subrgunit  16806  issubrg2  16808  abvdiv  16845  lss1  16941  lsssn0  16950  islss3  16961  prdslmodd  16971  islmhm2  17040  lspsolv  17145  lbsextlem4  17163  sralmod  17189  issubassa  17316  sraassa  17317  psrbaglesupp  17368  psrbaglesuppOLD  17369  psrbagcon  17373  psrgrp  17402  psrlmod  17405  psrrng  17416  psrassa  17419  mpllsslem  17444  mpllsslemOLD  17446  ipdi  17910  ipsubdir  17912  ipsubdi  17913  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  t1sep  18815  regsep2  18821  dnsconst  18823  dfcon2  18864  dislly  18942  tx1stc  19064  qtophmeo  19231  filss  19267  infil  19277  fsubbas  19281  filssufilg  19325  hauspwpwf1  19401  cnextcn  19480  tmdcn2  19501  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  met2ndci  19938  ngprcan  20042  ngplcan  20043  ngpsubcan  20046  nrgdsdi  20087  nrgdsdir  20088  nlmdsdi  20103  nlmdsdir  20104  blcvx  20216  iocopnst  20353  icccvx  20363  pi1grplem  20462  pi1xfrf  20466  pi1cof  20472  cvsdiv  20522  cvsdivcl  20523  cphdivcl  20542  cphsubdir  20567  cphsubdi  20568  bcthlem5  20680  rrxcph  20737  volfiniun  20869  volcn  20927  itg1val2  21003  dvconst  21232  dvlip  21306  ftc1a  21350  ulmdvlem3  21751  ang180  22094  cvxcl  22262  scvxcvx  22263  sgmmul  22424  logexprlim  22448  dchrabl  22477  f1otrge  22940  xmstrkgc  22954  colinearalglem1  22974  colinearalg  22978  axcgrtr  22983  axlowdimlem16  23025  axeuclidlem  23030  axcontlem4  23035  axcontlem7  23038  axcontlem12  23043  eengtrkg  23053  eengtrkge  23054  isspthonpth  23305  wlkdvspth  23329  grpomuldivass  23558  grpopnpcan2  23562  grponpncan  23564  grpodiveq  23565  ablodivdiv4  23600  ablonnncan  23602  ismndo1  23653  nvsubadd  23857  dipdi  24065  dipsubdi  24071  disjdsct  25821  omndmul2  25998  archiabllem2c  26035  srgi  26046  dvrdir  26110  dvrcan5  26113  kerf1hrm  26144  reofld  26161  pstmfval  26176  qqhval2lem  26263  qqhvq  26269  esumcvg  26388  sigaclcu  26413  measdivcstOLD  26491  measdivcst  26492  erdszelem9  26934  cvmseu  27012  cgrid2  27880  btwncomim  27890  btwnswapid  27894  trisegint  27905  cgrxfr  27932  btwnxfr  27933  brofs2  27954  brifs2  27955  endofsegid  27962  btwnconn1lem11  27974  btwnconn2  27979  segcon2  27982  seglemin  27990  segletr  27991  btwnsegle  27994  colinbtwnle  27995  broutsideof2  27999  btwnoutside  28002  broutsideof3  28003  outsideoftr  28006  outsidele  28009  ellines  28029  linethrueu  28033  ftc1anc  28316  sdclem1  28480  sstotbnd2  28514  zerdivemp1x  28602  isdrngo2  28605  iscringd  28640  irrapxlem6  29010  jm2.26lem3  29192  mpaamn  29355  mendrng  29391  mendlmod  29392  mendassa  29393  rfcnpre4  29598  fmuldfeq  29606  stoweidlem43  29681  stoweidlem52  29690  stoweidlem53  29691  stoweidlem56  29694  modfsummods  30087  usg2wotspth  30246  2pthwlkonot  30247  rusgranumwwlkg  30420  numclwwlk5  30548  friendship  30558  linccl  30654  lincsumscmcl  30673  lincresunit3lem1  30719  bnj970  31639  bnj910  31640  lsmsat  32223  lfladdcl  32286  lflnegcl  32290  lflvscl  32292  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  cvlexch3  32547  cvlexch4N  32548  cvlatexchb1  32549  cvlsupr2  32558  hlatjass  32584  hlatj12  32585  hlatj32  32586  cvrat  32636  atcvrj0  32642  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  islpln2a  32762  llncvrlpln  32772  lplncmp  32776  3atnelvolN  32800  4atlem11  32823  lplncvrlvol  32830  lvolcmp  32831  2atm2atN  32999  elpaddatriN  33017  elpadd2at2  33021  paddasslem8  33041  paddasslem17  33050  paddass  33052  padd12N  33053  paddssw1  33057  pmodlem2  33061  pmodN  33064  pmapjlln1  33069  atmod1i2  33073  pexmidlem2N  33185  pexmidlem7N  33190  pl42lem2N  33194  pl42lem3N  33195  pl42lem4N  33196  pl42N  33197  lhp2lt  33215  lhpm0atN  33243  lautlt  33305  lautcvr  33306  lautj  33307  lautm  33308  ltrneq2  33362  cdleme1b  33440  cdleme3b  33443  cdleme3c  33444  cdleme9b  33466  cdlemefs27cl  33627  cdleme42mN  33701  cdlemg4c  33826  trljco  33954  tgrpgrplem  33963  tendoplass  33997  tendodi1  33998  tendodi2  33999  erngplus2  34018  erngplus2-rN  34026  cdlemk36  34127  erngdvlem3  34204  erngdvlem3-rN  34212  dvaplusgv  34224  tendospass  34234  tendospdi1  34235  dvalveclem  34240  dialss  34261  dvhvaddass  34312  dvhopvsca  34317  dvhlveclem  34323  diblss  34385  diclss  34408  diclspsn  34409  cdlemn11pre  34425  dihmeetlem12N  34533  dihmeetlem16N  34537  dihmeetlem17N  34538  dvh4dimN  34662  lpolsatN  34703  lpolpolsatN  34704  dochpolN  34705  lclkr  34748  lclkrs  34754  lcfr  34800
  Copyright terms: Public domain W3C validator