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

Theorem simpr3 1005
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 999 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 464 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 974
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 369  df-3an 976
This theorem is referenced by:  simplr3  1041  simprr3  1047  simp1r3  1095  simp2r3  1101  simp3r3  1107  3anandis  1332  fpr2g  6111  isopolem  6223  fr3nr  6596  suppfnss  6927  elfir  7908  intrnfi  7909  fisupcl  7960  cnfcomlem  8174  cnfcomlemOLD  8182  ackbij1lem15  8645  pwfseqlem4a  9068  pwfseqlem4  9069  eluzuzle  11134  xlesubadd  11507  elioc2  11639  elico2  11640  elicc2  11641  fseq1p1m1  11805  ccatswrd  12735  modfsummods  13756  tanadd  14109  dvds2ln  14221  cshwsidrepsw  14785  ressress  14904  f1ovscpbl  15138  mreexexlem4d  15259  mreexexd  15260  2oppccomf  15336  fthmon  15538  fuccocl  15575  fucidcl  15576  invfuc  15585  initoeu2lem1  15615  curf2cl  15822  yonedalem4c  15868  yonedalem3  15871  pospo  15925  latjle12  16014  latjlej1  16017  latnlej2  16023  latlem12  16030  latmlem1  16033  latledi  16041  latjass  16047  latj12  16048  latj32  16049  latj13  16050  latj31  16051  latjrot  16052  latjjdi  16055  latjjdir  16056  latdisdlem  16141  prdsmndd  16275  imasmnd2  16279  imasmnd  16280  frmdmnd  16349  grpsubadd  16448  grpaddsubass  16450  grpsubsub4  16453  grppnpcan2  16454  grpnpncan  16455  grpnnncan2  16457  mulgnndir  16486  mulgnn0dir  16487  mulgnnass  16492  mulgnn0ass  16493  mulgass  16494  pwsmulg  16506  imasgrp2  16507  imasgrp  16508  issubg2  16538  qusgrp  16578  galcan  16664  gacan  16665  oppgmnd  16711  symggrp  16747  pmtrprfv  16800  pmtr3ncom  16822  psgnunilem3  16843  frgp0  17100  cmn32  17138  cmn12  17140  abladdsub  17147  mulgdi  17157  mulgsubdi  17160  dprdss  17394  dprdf1o  17397  dprdsn  17401  dmdprdsplit  17414  pgpfac1lem5  17448  srgi  17481  ringi  17529  prdsringd  17579  imasring  17586  opprring  17598  mulgass3  17604  dvrass  17657  kerf1hrm  17710  subrgunit  17765  issubrg2  17767  abvdiv  17804  lss1  17903  lsssn0  17912  islss3  17923  prdslmodd  17933  islmhm2  18002  lspsolv  18107  lbsextlem4  18125  sralmod  18151  issubassa  18291  sraassa  18292  psrbaglesupp  18335  psrbaglesuppOLD  18336  psrbagcon  18340  psrgrp  18369  psrlmod  18372  psrring  18384  psrassa  18387  mpllsslem  18412  mpllsslemOLD  18414  ipdi  18971  ipsubdir  18973  ipsubdi  18974  ipassr  18977  ipassr2  18978  isphld  18985  ocvlss  18999  mamudm  19180  matring  19235  matassa  19236  ofco2  19243  scmatlss  19317  ma1repveval  19363  mdetunilem1  19404  mdetunilem9  19412  monmatcollpw  19570  iinopn  19701  restopnb  19967  subbascn  20046  nrmsep2  20148  isnrm3  20151  t1sep  20162  regsep2  20168  dnsconst  20170  dfcon2  20210  dislly  20288  tx1stc  20441  qtophmeo  20608  filss  20644  infil  20654  fsubbas  20658  filssufilg  20702  hauspwpwf1  20778  cnextcn  20857  tmdcn2  20878  psmettri  21105  isxmet2d  21120  xmettri  21144  xmetres2  21154  bldisj  21191  blss2ps  21196  blss2  21197  xmstri2  21259  mstri2  21260  xmstri  21261  mstri  21262  xmstri3  21263  mstri3  21264  msrtri  21265  comet  21306  met2ndci  21315  ngprcan  21419  ngplcan  21420  ngpsubcan  21423  nrgdsdi  21464  nrgdsdir  21465  nlmdsdi  21480  nlmdsdir  21481  blcvx  21593  iocopnst  21730  icccvx  21740  pi1grplem  21839  pi1xfrf  21843  pi1cof  21849  cvsdiv  21899  cvsdivcl  21900  cphdivcl  21919  cphsubdir  21944  cphsubdi  21945  bcthlem5  22057  rrxcph  22114  volfiniun  22247  volcn  22305  itg1val2  22381  dvconst  22610  dvlip  22684  ftc1a  22728  ulmdvlem3  23087  ang180  23471  cvxcl  23638  scvxcvx  23639  sgmmul  23855  logexprlim  23879  dchrabl  23908  motgrp  24311  cgrane2  24555  cgrane4  24557  cgrahl1  24558  cgrahl2  24559  cgracgr  24560  cgratr  24565  dfcgra2  24566  f1otrge  24579  xmstrkgc  24593  colinearalglem1  24613  colinearalg  24617  axcgrtr  24622  axlowdimlem16  24664  axeuclidlem  24669  axcontlem4  24674  axcontlem7  24677  axcontlem12  24682  eengtrkg  24692  eengtrkge  24693  isspthonpth  24990  wlkdvspth  25014  usg2wotspth  25288  2pthwlkonot  25289  rusgranumwwlkg  25363  numclwwlk5  25516  friendship  25526  grpomuldivass  25651  grpopnpcan2  25655  grponpncan  25657  grpodiveq  25658  ablodivdiv4  25693  ablonnncan  25695  ismndo1  25746  nvsubadd  25950  dipdi  26158  dipsubdi  26164  disjdsct  27951  omndmul2  28140  archiabllem2c  28177  dvrdir  28219  dvrcan5  28222  reofld  28269  pstmfval  28314  qqhval2lem  28400  qqhvq  28406  esumcvg  28519  sigaclcu  28551  measdivcstOLD  28658  measdivcst  28659  carsggect  28752  bnj970  29319  bnj910  29320  erdszelem9  29483  cvmseu  29560  elmrsubrn  29719  cgrid2  30328  btwncomim  30338  btwnswapid  30342  trisegint  30353  cgrxfr  30380  btwnxfr  30381  brofs2  30402  brifs2  30403  endofsegid  30410  btwnconn1lem11  30422  btwnconn2  30427  segcon2  30430  seglemin  30438  segletr  30439  btwnsegle  30442  colinbtwnle  30443  broutsideof2  30447  btwnoutside  30450  broutsideof3  30451  outsideoftr  30454  outsidele  30457  ellines  30477  linethrueu  30481  ftc1anc  31451  sdclem1  31498  sstotbnd2  31532  zerdivemp1x  31620  isdrngo2  31623  iscringd  31658  lsmsat  32006  lfladdcl  32069  lflnegcl  32073  lflvscl  32075  lshpkrlem4  32111  lshpkrlem6  32113  ldualgrplem  32143  lduallmodlem  32150  latmassOLD  32227  latm12  32228  latm32  32229  latmrot  32230  latmmdiN  32232  latmmdir  32233  omlfh1N  32256  omlfh3N  32257  cvrnbtwn2  32273  cvlexchb1  32328  cvlexch3  32330  cvlexch4N  32331  cvlatexchb1  32332  cvlsupr2  32341  hlatjass  32367  hlatj12  32368  hlatj32  32369  cvrat  32419  atcvrj0  32425  cvrat2  32426  atltcvr  32432  atexchltN  32438  cvrat3  32439  cvrat4  32440  atbtwnexOLDN  32444  atbtwnex  32445  3dimlem3  32458  3dimlem3OLDN  32459  3at  32487  2atneat  32512  llncmp  32519  2at0mat0  32522  2atmat0  32523  islpln2a  32545  llncvrlpln  32555  lplncmp  32559  3atnelvolN  32583  4atlem11  32606  lplncvrlvol  32613  lvolcmp  32614  2atm2atN  32782  elpaddatriN  32800  elpadd2at2  32804  paddasslem8  32824  paddasslem17  32833  paddass  32835  padd12N  32836  paddssw1  32840  pmodlem2  32844  pmodN  32847  pmapjlln1  32852  atmod1i2  32856  pexmidlem2N  32968  pexmidlem7N  32973  pl42lem2N  32977  pl42lem3N  32978  pl42lem4N  32979  pl42N  32980  lhp2lt  32998  lhpm0atN  33026  lautlt  33088  lautcvr  33089  lautj  33090  lautm  33091  ltrneq2  33145  cdleme1b  33224  cdleme3b  33227  cdleme3c  33228  cdleme9b  33250  cdlemefs27cl  33412  cdleme42mN  33486  cdlemg4c  33611  trljco  33739  tgrpgrplem  33748  tendoplass  33782  tendodi1  33783  tendodi2  33784  erngplus2  33803  erngplus2-rN  33811  cdlemk36  33912  erngdvlem3  33989  erngdvlem3-rN  33997  dvaplusgv  34009  tendospass  34019  tendospdi1  34020  dvalveclem  34025  dialss  34046  dvhvaddass  34097  dvhopvsca  34102  dvhlveclem  34108  diblss  34170  diclss  34193  diclspsn  34194  cdlemn11pre  34210  dihmeetlem12N  34318  dihmeetlem16N  34322  dihmeetlem17N  34323  dvh4dimN  34447  lpolsatN  34488  lpolpolsatN  34489  dochpolN  34490  lclkr  34533  lclkrs  34539  lcfr  34585  irrapxlem6  35104  jm2.26lem3  35285  mpaamn  35449  mendring  35485  mendlmod  35486  mendassa  35487  rfcnpre4  36769  fmuldfeq  36926  stoweidlem43  37174  stoweidlem52  37183  stoweidlem53  37184  stoweidlem56  37187  iccelpart  37681  pfxccat3a  37897  copissgrp  38106  ringrng  38177  cznrng  38255  funcringcsetcALTV2lem9  38344  funcringcsetclem9ALTV  38367  linccl  38507  lincsumscmcl  38526  ldepsprlem  38565  lincresunit3lem1  38572
  Copyright terms: Public domain W3C validator