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

Theorem simpr3 996
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 990 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 466 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965
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 967
This theorem is referenced by:  simplr3  1032  simprr3  1038  simp1r3  1086  simp2r3  1092  simp3r3  1098  3anandis  1320  isopolem  6031  fr3nr  6386  suppfnss  6709  elfir  7657  intrnfi  7658  fisupcl  7709  cnfcomlem  7924  cnfcomlemOLD  7932  ackbij1lem15  8395  pwfseqlem4a  8820  pwfseqlem4  8821  xlesubadd  11218  elioc2  11350  elico2  11351  elicc2  11352  fseq1p1m1  11526  swrdsymbeq  12333  ccatswrd  12342  tanadd  13443  dvds2ln  13555  cshwsidrepsw  14112  ressress  14227  f1ovscpbl  14456  mreexexlem4d  14577  mreexexd  14578  2oppccomf  14656  fthmon  14829  fuccocl  14866  fucidcl  14867  invfuc  14876  curf2cl  15033  yonedalem4c  15079  yonedalem3  15082  pospo  15135  latjle12  15224  latjlej1  15227  latnlej2  15233  latlem12  15240  latmlem1  15243  latledi  15251  latjass  15257  latj12  15258  latj32  15259  latj13  15260  latj31  15261  latjrot  15262  latjjdi  15265  latjjdir  15266  latdisdlem  15351  prdsmndd  15446  imasmnd2  15450  imasmnd  15451  frmdmnd  15528  grpsubadd  15604  grpaddsubass  15606  grpsubsub4  15609  grppnpcan2  15610  grpnpncan  15611  grpnnncan2  15612  mulgnndir  15640  mulgnn0dir  15641  mulgnnass  15646  mulgnn0ass  15647  mulgass  15648  pwsmulg  15660  imasgrp2  15661  imasgrp  15662  issubg2  15687  divsgrp  15727  galcan  15813  gacan  15814  oppgmnd  15860  symggrp  15896  pmtrprfv  15950  pmtr3ncom  15972  psgnunilem3  15993  frgp0  16248  cmn32  16286  cmn12  16288  abladdsub  16295  mulgdi  16305  mulgsubdi  16308  dprdss  16514  dprdf1o  16517  dprdsn  16521  dmdprdsplit  16534  pgpfac1lem5  16568  srgi  16601  rngi  16645  prdsrngd  16692  imasrng  16699  opprrng  16711  mulgass3  16717  dvrass  16770  subrgunit  16861  issubrg2  16863  abvdiv  16900  lss1  16997  lsssn0  17006  islss3  17017  prdslmodd  17027  islmhm2  17096  lspsolv  17201  lbsextlem4  17219  sralmod  17245  issubassa  17372  sraassa  17373  psrbaglesupp  17412  psrbaglesuppOLD  17413  psrbagcon  17417  psrgrp  17446  psrlmod  17449  psrrng  17460  psrassa  17463  mpllsslem  17488  mpllsslemOLD  17490  ipdi  18044  ipsubdir  18046  ipsubdi  18047  ipassr  18050  ipassr2  18051  isphld  18058  ocvlss  18072  mamudm  18263  matrng  18305  matassa  18306  ofco2  18307  ma1repveval  18357  mdetunilem1  18393  mdetunilem9  18401  iinopn  18490  restopnb  18754  subbascn  18833  nrmsep2  18935  isnrm3  18938  t1sep  18949  regsep2  18955  dnsconst  18957  dfcon2  18998  dislly  19076  tx1stc  19198  qtophmeo  19365  filss  19401  infil  19411  fsubbas  19415  filssufilg  19459  hauspwpwf1  19535  cnextcn  19614  tmdcn2  19635  psmettri  19862  isxmet2d  19877  xmettri  19901  xmetres2  19911  bldisj  19948  blss2ps  19953  blss2  19954  xmstri2  20016  mstri2  20017  xmstri  20018  mstri  20019  xmstri3  20020  mstri3  20021  msrtri  20022  comet  20063  met2ndci  20072  ngprcan  20176  ngplcan  20177  ngpsubcan  20180  nrgdsdi  20221  nrgdsdir  20222  nlmdsdi  20237  nlmdsdir  20238  blcvx  20350  iocopnst  20487  icccvx  20497  pi1grplem  20596  pi1xfrf  20600  pi1cof  20606  cvsdiv  20656  cvsdivcl  20657  cphdivcl  20676  cphsubdir  20701  cphsubdi  20702  bcthlem5  20814  rrxcph  20871  volfiniun  21003  volcn  21061  itg1val2  21137  dvconst  21366  dvlip  21440  ftc1a  21484  ulmdvlem3  21842  ang180  22185  cvxcl  22353  scvxcvx  22354  sgmmul  22515  logexprlim  22539  dchrabl  22568  f1otrge  23069  xmstrkgc  23083  colinearalglem1  23103  colinearalg  23107  axcgrtr  23112  axlowdimlem16  23154  axeuclidlem  23159  axcontlem4  23164  axcontlem7  23167  axcontlem12  23172  eengtrkg  23182  eengtrkge  23183  isspthonpth  23434  wlkdvspth  23458  grpomuldivass  23687  grpopnpcan2  23691  grponpncan  23693  grpodiveq  23694  ablodivdiv4  23729  ablonnncan  23731  ismndo1  23782  nvsubadd  23986  dipdi  24194  dipsubdi  24200  disjdsct  25949  omndmul2  26126  archiabllem2c  26163  dvrdir  26209  dvrcan5  26212  kerf1hrm  26243  reofld  26260  pstmfval  26275  qqhval2lem  26362  qqhvq  26368  esumcvg  26487  sigaclcu  26512  measdivcstOLD  26590  measdivcst  26591  erdszelem9  27039  cvmseu  27117  cgrid2  27985  btwncomim  27995  btwnswapid  27999  trisegint  28010  cgrxfr  28037  btwnxfr  28038  brofs2  28059  brifs2  28060  endofsegid  28067  btwnconn1lem11  28079  btwnconn2  28084  segcon2  28087  seglemin  28095  segletr  28096  btwnsegle  28099  colinbtwnle  28100  broutsideof2  28104  btwnoutside  28107  broutsideof3  28108  outsideoftr  28111  outsidele  28114  ellines  28134  linethrueu  28138  ftc1anc  28428  sdclem1  28592  sstotbnd2  28626  zerdivemp1x  28714  isdrngo2  28717  iscringd  28752  irrapxlem6  29121  jm2.26lem3  29303  mpaamn  29466  mendrng  29502  mendlmod  29503  mendassa  29504  rfcnpre4  29709  fmuldfeq  29717  stoweidlem43  29791  stoweidlem52  29800  stoweidlem53  29801  stoweidlem56  29804  modfsummods  30197  usg2wotspth  30356  2pthwlkonot  30357  rusgranumwwlkg  30530  numclwwlk5  30658  friendship  30668  linccl  30837  lincsumscmcl  30856  lincresunit3lem1  30902  bnj970  31827  bnj910  31828  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  33710  cdleme3b  33713  cdleme3c  33714  cdleme9b  33736  cdlemefs27cl  33897  cdleme42mN  33971  cdlemg4c  34096  trljco  34224  tgrpgrplem  34233  tendoplass  34267  tendodi1  34268  tendodi2  34269  erngplus2  34288  erngplus2-rN  34296  cdlemk36  34397  erngdvlem3  34474  erngdvlem3-rN  34482  dvaplusgv  34494  tendospass  34504  tendospdi1  34505  dvalveclem  34510  dialss  34531  dvhvaddass  34582  dvhopvsca  34587  dvhlveclem  34593  diblss  34655  diclss  34678  diclspsn  34679  cdlemn11pre  34695  dihmeetlem12N  34803  dihmeetlem16N  34807  dihmeetlem17N  34808  dvh4dimN  34932  lpolsatN  34973  lpolpolsatN  34974  dochpolN  34975  lclkr  35018  lclkrs  35024  lcfr  35070
  Copyright terms: Public domain W3C validator