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

Theorem simpr3 963
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 957 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 452 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  simplr3  999  simprr3  1005  simp1r3  1053  simp2r3  1059  simp3r3  1065  3anandis  1283  fr3nr  4571  isopolem  5842  elfir  7169  intrnfi  7170  fisupcl  7218  cnfcomlem  7402  ackbij1lem15  7860  pwfseqlem4a  8283  pwfseqlem4  8284  xlesubadd  10583  elioc2  10713  elico2  10714  elicc2  10715  fseq1p1m1  10857  ccatswrd  11459  tanadd  12447  dvds2ln  12559  ressress  13205  f1ovscpbl  13428  mreexexlem4d  13549  mreexexd  13550  2oppccomf  13628  fthmon  13801  fuccocl  13838  fucidcl  13839  invfuc  13848  curf2cl  14005  yonedalem4c  14051  yonedalem3  14054  pospo  14107  latjlej1  14171  latnlej2  14177  latmlem1  14187  latledi  14195  latjass  14201  latj12  14202  latj32  14203  latj13  14204  latj31  14205  latjrot  14206  latjjdi  14209  latjjdir  14210  latdisdlem  14292  prdsmndd  14405  imasmnd2  14409  imasmnd  14410  frmdmnd  14481  grpsubadd  14553  grpaddsubass  14555  grpsubsub4  14558  grppnpcan2  14559  grpnpncan  14560  grpnnncan2  14561  mulgnndir  14589  mulgnn0dir  14590  mulgnnass  14595  mulgnn0ass  14596  mulgass  14597  pwsmulg  14609  imasgrp2  14610  imasgrp  14611  issubg2  14636  divsgrp  14672  galcan  14758  gacan  14759  symggrp  14780  oppgmnd  14827  frgp0  15069  cmn32  15107  cmn12  15109  abladdsub  15116  mulgdi  15126  mulgsubdi  15129  dprdss  15264  dprdf1o  15267  dprdsn  15271  dmdprdsplit  15282  pgpfac1lem5  15314  rngi  15353  prdsrngd  15395  imasrng  15402  opprrng  15413  mulgass3  15419  dvrass  15472  subrgunit  15563  issubrg2  15565  abvdiv  15602  lss1  15696  lsssn0  15705  islss3  15716  prdslmodd  15726  islmhm2  15795  lspsolv  15896  lbsextlem4  15914  sralmod  15939  issubassa  16064  sraassa  16065  psrbaglesupp  16114  psrbagcon  16117  psrgrp  16143  psrlmod  16146  psrrng  16155  psrassa  16158  mpllsslem  16180  ipdi  16544  ipsubdir  16546  ipsubdi  16547  ipassr  16550  ipassr2  16551  isphld  16558  ocvlss  16572  iinopn  16648  restopnb  16906  subbascn  16984  nrmsep2  17084  isnrm3  17087  t1sep  17098  regsep2  17104  dnsconst  17106  dfcon2  17145  dislly  17223  tx1stc  17344  qtophmeo  17508  filss  17548  infil  17558  fsubbas  17562  filssufilg  17606  hauspwpwf1  17682  tmdcn2  17772  isxmet2d  17892  xmettri  17915  xmetres2  17925  bldisj  17955  blss2  17959  xmstri2  18012  mstri2  18013  xmstri  18014  mstri  18015  xmstri3  18016  mstri3  18017  msrtri  18018  comet  18059  met2ndci  18068  ngprcan  18131  ngplcan  18132  ngpsubcan  18135  nrgdsdi  18176  nrgdsdir  18177  nlmdsdi  18192  nlmdsdir  18193  blcvx  18304  iocopnst  18438  icccvx  18448  pi1grplem  18547  pi1xfrf  18551  pi1cof  18557  cphdivcl  18618  cphsubdir  18643  cphsubdi  18644  bcthlem5  18750  volfiniun  18904  volcn  18961  itg1val2  19039  dvconst  19266  dvlip  19340  ftc1a  19384  ulmdvlem3  19779  ang180  20112  cvxcl  20279  scvxcvx  20280  sgmmul  20440  logexprlim  20464  dchrabl  20493  grpomuldivass  20916  grpopnpcan2  20920  grponpncan  20922  grpodiveq  20923  ablodivdiv4  20958  ablonnncan  20960  ismndo1  21011  nvsubadd  21213  dipdi  21421  dipsubdi  21427  disjdsct  23369  esumcvg  23454  measdivcstOLD  23551  measdivcst  23552  erdszelem9  23730  cvmseu  23807  colinearalglem1  24534  colinearalg  24538  axcgrtr  24543  axlowdimlem16  24585  axeuclidlem  24590  axcontlem4  24595  axcontlem7  24598  axcontlem12  24603  cgrid2  24626  btwncomim  24636  btwnswapid  24640  trisegint  24651  cgrxfr  24678  btwnxfr  24679  brofs2  24700  brifs2  24701  endofsegid  24708  btwnconn1lem11  24720  btwnconn2  24725  segcon2  24728  seglemin  24736  segletr  24737  btwnsegle  24740  colinbtwnle  24741  broutsideof2  24745  btwnoutside  24748  broutsideof3  24749  outsideoftr  24752  outsidele  24755  ellines  24775  linethrueu  24779  copsexgb  24966  iccss3  25134  reacomsmgrp2  25344  reacomsmgrp3  25345  grpodlcan  25376  rltrran  25414  dblsubvec  25474  mvecrtol2  25477  cnrsfin  25525  cnrscoa  25526  cmptdst  25568  cmptdst2  25571  usinuniopb  25594  lvsovso  25626  addassv  25656  icccon2  25700  iepiclem  25823  cmpsubc  25856  sdclem1  26453  sstotbnd2  26498  zerdivemp1x  26586  isdrngo2  26589  iscringd  26624  irrapxlem6  26912  jm2.26lem3  27094  mpaamn  27361  pmtrprfv  27396  psgnunilem3  27419  matrng  27480  matassa  27481  mendrng  27500  mendlmod  27501  mendassa  27502  rfcnpre4  27705  fmuldfeq  27713  stoweidlem43  27792  stoweidlem52  27801  stoweidlem53  27802  stoweidlem56  27805  bnj970  28979  bnj910  28980  lsmsat  29198  lfladdcl  29261  lflnegcl  29265  lflvscl  29267  lshpkrlem4  29303  lshpkrlem6  29305  ldualgrplem  29335  lduallmodlem  29342  latmassOLD  29419  latm12  29420  latm32  29421  latmrot  29422  latmmdiN  29424  latmmdir  29425  omlfh1N  29448  omlfh3N  29449  cvrnbtwn2  29465  cvlexchb1  29520  cvlexch3  29522  cvlexch4N  29523  cvlatexchb1  29524  cvlsupr2  29533  hlatjass  29559  hlatj12  29560  hlatj32  29561  cvrat  29611  atcvrj0  29617  cvrat2  29618  atltcvr  29624  atexchltN  29630  cvrat3  29631  cvrat4  29632  atbtwnexOLDN  29636  atbtwnex  29637  3dimlem3  29650  3dimlem3OLDN  29651  3at  29679  2atneat  29704  llncmp  29711  2at0mat0  29714  2atmat0  29715  islpln2a  29737  llncvrlpln  29747  lplncmp  29751  3atnelvolN  29775  4atlem11  29798  lplncvrlvol  29805  lvolcmp  29806  2atm2atN  29974  elpaddatriN  29992  elpadd2at2  29996  paddasslem8  30016  paddasslem17  30025  paddass  30027  padd12N  30028  paddssw1  30032  pmodlem2  30036  pmodN  30039  pmapjlln1  30044  atmod1i2  30048  pexmidlem2N  30160  pexmidlem7N  30165  pl42lem2N  30169  pl42lem3N  30170  pl42lem4N  30171  pl42N  30172  lhp2lt  30190  lhpm0atN  30218  lautlt  30280  lautcvr  30281  lautj  30282  lautm  30283  ltrneq2  30337  cdleme1b  30415  cdleme3b  30418  cdleme3c  30419  cdleme9b  30441  cdlemefs27cl  30602  cdleme42mN  30676  cdlemg4c  30801  trljco  30929  tgrpgrplem  30938  tendoplass  30972  tendodi1  30973  tendodi2  30974  erngplus2  30993  erngplus2-rN  31001  cdlemk36  31102  erngdvlem3  31179  erngdvlem3-rN  31187  dvaplusgv  31199  tendospass  31209  tendospdi1  31210  dvalveclem  31215  dialss  31236  dvhvaddass  31287  dvhopvsca  31292  dvhlveclem  31298  diblss  31360  diclss  31383  diclspsn  31384  cdlemn11pre  31400  dihmeetlem12N  31508  dihmeetlem16N  31512  dihmeetlem17N  31513  dvh4dimN  31637  lpolsatN  31678  lpolpolsatN  31679  dochpolN  31680  lclkr  31723  lclkrs  31729  lcfr  31775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator