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

Theorem simpr3 1013
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 1007 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 467 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
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:  simplr3  1049  simprr3  1055  simp1r3  1103  simp2r3  1109  simp3r3  1115  3anandis  1366  fpr2g  6137  isopolem  6248  fr3nr  6617  suppfnss  6948  elfir  7932  intrnfi  7933  fisupcl  7988  cnfcomlem  8206  ackbij1lem15  8665  pwfseqlem4a  9087  pwfseqlem4  9088  eluzuzle  11168  xlesubadd  11550  elioc2  11698  elico2  11699  elicc2  11700  fseq1p1m1  11869  ccatswrd  12803  modfsummods  13841  tanadd  14209  dvds2ln  14321  prmgaplem5  15013  prmgaplem8  15016  cshwsidrepsw  15052  ressress  15175  f1ovscpbl  15420  mreexexlem4d  15541  mreexexd  15542  2oppccomf  15618  fthmon  15820  fuccocl  15857  fucidcl  15858  invfuc  15867  initoeu2lem1  15897  curf2cl  16104  yonedalem4c  16150  yonedalem3  16153  pospo  16207  latjle12  16296  latjlej1  16299  latnlej2  16305  latlem12  16312  latmlem1  16315  latledi  16323  latjass  16329  latj12  16330  latj32  16331  latj13  16332  latj31  16333  latjrot  16334  latjjdi  16337  latjjdir  16338  latdisdlem  16423  prdsmndd  16557  imasmnd2  16561  imasmnd  16562  frmdmnd  16631  grpsubadd  16730  grpaddsubass  16732  grpsubsub4  16735  grppnpcan2  16736  grpnpncan  16737  grpnnncan2  16739  mulgnndir  16768  mulgnn0dir  16769  mulgnnass  16774  mulgnn0ass  16775  mulgass  16776  pwsmulg  16788  imasgrp2  16789  imasgrp  16790  issubg2  16820  qusgrp  16860  galcan  16946  gacan  16947  oppgmnd  16993  symggrp  17029  pmtrprfv  17082  pmtr3ncom  17104  psgnunilem3  17125  frgp0  17398  cmn32  17436  cmn12  17438  abladdsub  17445  mulgdi  17455  mulgsubdi  17458  dprdss  17650  dprdf1o  17653  dprdsn  17657  dmdprdsplit  17668  pgpfac1lem5  17700  srgi  17733  ringi  17781  prdsringd  17828  imasring  17835  opprring  17847  mulgass3  17853  dvrass  17906  kerf1hrm  17959  subrgunit  18014  issubrg2  18016  abvdiv  18053  lss1  18150  lsssn0  18159  islss3  18170  prdslmodd  18180  islmhm2  18249  lspsolv  18354  lbsextlem4  18372  sralmod  18398  issubassa  18536  sraassa  18537  psrbaglesupp  18580  psrbagcon  18583  psrgrp  18610  psrlmod  18613  psrring  18623  psrassa  18626  mpllsslem  18647  ipdi  19194  ipsubdir  19196  ipsubdi  19197  ipassr  19200  ipassr2  19201  isphld  19208  ocvlss  19222  mamudm  19400  matring  19455  matassa  19456  ofco2  19463  scmatlss  19537  ma1repveval  19583  mdetunilem1  19624  mdetunilem9  19632  monmatcollpw  19790  iinopn  19919  restopnb  20178  subbascn  20257  nrmsep2  20359  isnrm3  20362  t1sep  20373  regsep2  20379  dnsconst  20381  dfcon2  20421  dislly  20499  tx1stc  20652  qtophmeo  20819  filss  20855  infil  20865  fsubbas  20869  filssufilg  20913  hauspwpwf1  20989  cnextcn  21069  tmdcn2  21091  psmettri  21314  isxmet2d  21329  xmettri  21353  xmetres2  21363  bldisj  21400  blss2ps  21405  blss2  21406  xmstri2  21468  mstri2  21469  xmstri  21470  mstri  21471  xmstri3  21472  mstri3  21473  msrtri  21474  comet  21515  met2ndci  21524  ngprcan  21610  ngplcan  21611  ngpsubcan  21614  nrgdsdi  21655  nrgdsdir  21656  nlmdsdi  21671  nlmdsdir  21672  blcvx  21803  iocopnst  21955  icccvx  21965  pi1grplem  22067  pi1xfrf  22071  pi1cof  22077  cvsdiv  22127  cvsdivcl  22128  cphdivcl  22147  cphsubdir  22172  cphsubdi  22173  bcthlem5  22283  rrxcph  22338  volfiniun  22487  volcn  22551  itg1val2  22629  dvconst  22858  dvlip  22932  ftc1a  22976  ulmdvlem3  23344  ang180  23730  cvxcl  23897  scvxcvx  23898  sgmmul  24116  logexprlim  24140  dchrabl  24169  motgrp  24575  iscgra1  24839  cgrane2  24842  cgrane4  24844  cgrahl1  24845  cgrahl2  24846  cgracgr  24847  cgratr  24852  cgrabtwn  24854  cgrahl  24855  dfcgra2  24858  sacgr  24859  f1otrge  24889  xmstrkgc  24903  colinearalglem1  24923  colinearalg  24927  axcgrtr  24932  axlowdimlem16  24974  axeuclidlem  24979  axcontlem4  24984  axcontlem7  24987  axcontlem12  24992  eengtrkg  25002  eengtrkge  25003  isspthonpth  25300  wlkdvspth  25324  usg2wotspth  25598  2pthwlkonot  25599  rusgranumwwlkg  25673  numclwwlk5  25826  friendship  25836  grpomuldivass  25963  grpopnpcan2  25967  grponpncan  25969  grpodiveq  25970  ablodivdiv4  26005  ablonnncan  26007  ismndo1  26058  nvsubadd  26262  dipdi  26470  dipsubdi  26476  disjdsct  28273  omndmul2  28470  archiabllem2c  28507  dvrdir  28549  dvrcan5  28552  reofld  28599  pstmfval  28695  qqhval2lem  28781  qqhvq  28787  esumcvg  28903  sigaclcu  28935  measdivcstOLD  29042  measdivcst  29043  carsggect  29146  bnj970  29754  bnj910  29755  erdszelem9  29918  cvmseu  29995  elmrsubrn  30154  cgrid2  30763  btwncomim  30773  btwnswapid  30777  trisegint  30788  cgrxfr  30815  btwnxfr  30816  brofs2  30837  brifs2  30838  endofsegid  30845  btwnconn1lem11  30857  btwnconn2  30862  segcon2  30865  seglemin  30873  segletr  30874  btwnsegle  30877  colinbtwnle  30878  broutsideof2  30882  btwnoutside  30885  broutsideof3  30886  outsideoftr  30889  outsidele  30892  ellines  30912  linethrueu  30916  poimirlem28  31882  ftc1anc  31939  sdclem1  31986  sstotbnd2  32020  zerdivemp1x  32108  isdrngo2  32111  iscringd  32146  lsmsat  32493  lfladdcl  32556  lflnegcl  32560  lflvscl  32562  lshpkrlem4  32598  lshpkrlem6  32600  ldualgrplem  32630  lduallmodlem  32637  latmassOLD  32714  latm12  32715  latm32  32716  latmrot  32717  latmmdiN  32719  latmmdir  32720  omlfh1N  32743  omlfh3N  32744  cvrnbtwn2  32760  cvlexchb1  32815  cvlexch3  32817  cvlexch4N  32818  cvlatexchb1  32819  cvlsupr2  32828  hlatjass  32854  hlatj12  32855  hlatj32  32856  cvrat  32906  atcvrj0  32912  cvrat2  32913  atltcvr  32919  atexchltN  32925  cvrat3  32926  cvrat4  32927  atbtwnexOLDN  32931  atbtwnex  32932  3dimlem3  32945  3dimlem3OLDN  32946  3at  32974  2atneat  32999  llncmp  33006  2at0mat0  33009  2atmat0  33010  islpln2a  33032  llncvrlpln  33042  lplncmp  33046  3atnelvolN  33070  4atlem11  33093  lplncvrlvol  33100  lvolcmp  33101  2atm2atN  33269  elpaddatriN  33287  elpadd2at2  33291  paddasslem8  33311  paddasslem17  33320  paddass  33322  padd12N  33323  paddssw1  33327  pmodlem2  33331  pmodN  33334  pmapjlln1  33339  atmod1i2  33343  pexmidlem2N  33455  pexmidlem7N  33460  pl42lem2N  33464  pl42lem3N  33465  pl42lem4N  33466  pl42N  33467  lhp2lt  33485  lhpm0atN  33513  lautlt  33575  lautcvr  33576  lautj  33577  lautm  33578  ltrneq2  33632  cdleme1b  33711  cdleme3b  33714  cdleme3c  33715  cdleme9b  33737  cdlemefs27cl  33899  cdleme42mN  33973  cdlemg4c  34098  trljco  34226  tgrpgrplem  34235  tendoplass  34269  tendodi1  34270  tendodi2  34271  erngplus2  34290  erngplus2-rN  34298  cdlemk36  34399  erngdvlem3  34476  erngdvlem3-rN  34484  dvaplusgv  34496  tendospass  34506  tendospdi1  34507  dvalveclem  34512  dialss  34533  dvhvaddass  34584  dvhopvsca  34589  dvhlveclem  34595  diblss  34657  diclss  34680  diclspsn  34681  cdlemn11pre  34697  dihmeetlem12N  34805  dihmeetlem16N  34809  dihmeetlem17N  34810  dvh4dimN  34934  lpolsatN  34975  lpolpolsatN  34976  dochpolN  34977  lclkr  35020  lclkrs  35026  lcfr  35072  irrapxlem6  35591  jm2.26lem3  35776  mpaamn  35942  mendring  35978  mendlmod  35979  mendassa  35980  rfcnpre4  37216  fmuldfeq  37481  stoweidlem43  37724  stoweidlem52  37733  stoweidlem53  37734  stoweidlem56  37737  iccelpart  38459  pfxccat3a  38682  funopsn  38717  structiedg0val  38788  copissgrp  39080  ringrng  39151  cznrng  39229  funcringcsetcALTV2lem9  39318  funcringcsetclem9ALTV  39341  linccl  39481  lincsumscmcl  39500  ldepsprlem  39539  lincresunit3lem1  39546
  Copyright terms: Public domain W3C validator