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

Theorem simpr3 1016
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 1010 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 468 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371    /\ w3a 985
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 189  df-an 373  df-3an 987
This theorem is referenced by:  simplr3  1052  simprr3  1058  simp1r3  1106  simp2r3  1112  simp3r3  1118  3anandis  1371  fpr2g  6125  isopolem  6236  fr3nr  6606  suppfnss  6940  elfir  7929  intrnfi  7930  fisupcl  7985  cnfcomlem  8204  ackbij1lem15  8664  pwfseqlem4a  9086  pwfseqlem4  9087  eluzuzle  11167  xlesubadd  11549  elioc2  11697  elico2  11698  elicc2  11699  fseq1p1m1  11868  ccatswrd  12812  modfsummods  13853  tanadd  14221  dvds2ln  14333  prmgaplem5  15025  prmgaplem8  15028  cshwsidrepsw  15064  ressress  15187  f1ovscpbl  15432  mreexexlem4d  15553  mreexexd  15554  2oppccomf  15630  fthmon  15832  fuccocl  15869  fucidcl  15870  invfuc  15879  initoeu2lem1  15909  curf2cl  16116  yonedalem4c  16162  yonedalem3  16165  pospo  16219  latjle12  16308  latjlej1  16311  latnlej2  16317  latlem12  16324  latmlem1  16327  latledi  16335  latjass  16341  latj12  16342  latj32  16343  latj13  16344  latj31  16345  latjrot  16346  latjjdi  16349  latjjdir  16350  latdisdlem  16435  prdsmndd  16569  imasmnd2  16573  imasmnd  16574  frmdmnd  16643  grpsubadd  16742  grpaddsubass  16744  grpsubsub4  16747  grppnpcan2  16748  grpnpncan  16749  grpnnncan2  16751  mulgnndir  16780  mulgnn0dir  16781  mulgnnass  16786  mulgnn0ass  16787  mulgass  16788  pwsmulg  16800  imasgrp2  16801  imasgrp  16802  issubg2  16832  qusgrp  16872  galcan  16958  gacan  16959  oppgmnd  17005  symggrp  17041  pmtrprfv  17094  pmtr3ncom  17116  psgnunilem3  17137  frgp0  17410  cmn32  17448  cmn12  17450  abladdsub  17457  mulgdi  17467  mulgsubdi  17470  dprdss  17662  dprdf1o  17665  dprdsn  17669  dmdprdsplit  17680  pgpfac1lem5  17712  srgi  17745  ringi  17793  prdsringd  17840  imasring  17847  opprring  17859  mulgass3  17865  dvrass  17918  kerf1hrm  17971  subrgunit  18026  issubrg2  18028  abvdiv  18065  lss1  18162  lsssn0  18171  islss3  18182  prdslmodd  18192  islmhm2  18261  lspsolv  18366  lbsextlem4  18384  sralmod  18410  issubassa  18548  sraassa  18549  psrbaglesupp  18592  psrbagcon  18595  psrgrp  18622  psrlmod  18625  psrring  18635  psrassa  18638  mpllsslem  18659  ipdi  19207  ipsubdir  19209  ipsubdi  19210  ipassr  19213  ipassr2  19214  isphld  19221  ocvlss  19235  mamudm  19413  matring  19468  matassa  19469  ofco2  19476  scmatlss  19550  ma1repveval  19596  mdetunilem1  19637  mdetunilem9  19645  monmatcollpw  19803  iinopn  19932  restopnb  20191  subbascn  20270  nrmsep2  20372  isnrm3  20375  t1sep  20386  regsep2  20392  dnsconst  20394  dfcon2  20434  dislly  20512  tx1stc  20665  qtophmeo  20832  filss  20868  infil  20878  fsubbas  20882  filssufilg  20926  hauspwpwf1  21002  cnextcn  21082  tmdcn2  21104  psmettri  21327  isxmet2d  21342  xmettri  21366  xmetres2  21376  bldisj  21413  blss2ps  21418  blss2  21419  xmstri2  21481  mstri2  21482  xmstri  21483  mstri  21484  xmstri3  21485  mstri3  21486  msrtri  21487  comet  21528  met2ndci  21537  ngprcan  21623  ngplcan  21624  ngpsubcan  21627  nrgdsdi  21668  nrgdsdir  21669  nlmdsdi  21684  nlmdsdir  21685  blcvx  21816  iocopnst  21968  icccvx  21978  pi1grplem  22080  pi1xfrf  22084  pi1cof  22090  cvsdiv  22140  cvsdivcl  22141  cphdivcl  22160  cphsubdir  22185  cphsubdi  22186  bcthlem5  22296  rrxcph  22351  volfiniun  22500  volcn  22564  itg1val2  22642  dvconst  22871  dvlip  22945  ftc1a  22989  ulmdvlem3  23357  ang180  23743  cvxcl  23910  scvxcvx  23911  sgmmul  24129  logexprlim  24153  dchrabl  24182  motgrp  24588  iscgra1  24852  cgrane2  24855  cgrane4  24857  cgrahl1  24858  cgrahl2  24859  cgracgr  24860  cgratr  24865  cgrabtwn  24867  cgrahl  24868  dfcgra2  24871  sacgr  24872  f1otrge  24902  xmstrkgc  24916  colinearalglem1  24936  colinearalg  24940  axcgrtr  24945  axlowdimlem16  24987  axeuclidlem  24992  axcontlem4  24997  axcontlem7  25000  axcontlem12  25005  eengtrkg  25015  eengtrkge  25016  isspthonpth  25314  wlkdvspth  25338  usg2wotspth  25612  2pthwlkonot  25613  rusgranumwwlkg  25687  numclwwlk5  25840  friendship  25850  grpomuldivass  25977  grpopnpcan2  25981  grponpncan  25983  grpodiveq  25984  ablodivdiv4  26019  ablonnncan  26021  ismndo1  26072  nvsubadd  26276  dipdi  26484  dipsubdi  26490  disjdsct  28283  omndmul2  28475  archiabllem2c  28512  dvrdir  28553  dvrcan5  28556  reofld  28603  pstmfval  28699  qqhval2lem  28785  qqhvq  28791  esumcvg  28907  sigaclcu  28939  measdivcstOLD  29046  measdivcst  29047  carsggect  29150  bnj970  29758  bnj910  29759  erdszelem9  29922  cvmseu  29999  elmrsubrn  30158  cgrid2  30770  btwncomim  30780  btwnswapid  30784  trisegint  30795  cgrxfr  30822  btwnxfr  30823  brofs2  30844  brifs2  30845  endofsegid  30852  btwnconn1lem11  30864  btwnconn2  30869  segcon2  30872  seglemin  30880  segletr  30881  btwnsegle  30884  colinbtwnle  30885  broutsideof2  30889  btwnoutside  30892  broutsideof3  30893  outsideoftr  30896  outsidele  30899  ellines  30919  linethrueu  30923  poimirlem28  31968  ftc1anc  32025  sdclem1  32072  sstotbnd2  32106  zerdivemp1x  32194  isdrngo2  32197  iscringd  32232  lsmsat  32574  lfladdcl  32637  lflnegcl  32641  lflvscl  32643  lshpkrlem4  32679  lshpkrlem6  32681  ldualgrplem  32711  lduallmodlem  32718  latmassOLD  32795  latm12  32796  latm32  32797  latmrot  32798  latmmdiN  32800  latmmdir  32801  omlfh1N  32824  omlfh3N  32825  cvrnbtwn2  32841  cvlexchb1  32896  cvlexch3  32898  cvlexch4N  32899  cvlatexchb1  32900  cvlsupr2  32909  hlatjass  32935  hlatj12  32936  hlatj32  32937  cvrat  32987  atcvrj0  32993  cvrat2  32994  atltcvr  33000  atexchltN  33006  cvrat3  33007  cvrat4  33008  atbtwnexOLDN  33012  atbtwnex  33013  3dimlem3  33026  3dimlem3OLDN  33027  3at  33055  2atneat  33080  llncmp  33087  2at0mat0  33090  2atmat0  33091  islpln2a  33113  llncvrlpln  33123  lplncmp  33127  3atnelvolN  33151  4atlem11  33174  lplncvrlvol  33181  lvolcmp  33182  2atm2atN  33350  elpaddatriN  33368  elpadd2at2  33372  paddasslem8  33392  paddasslem17  33401  paddass  33403  padd12N  33404  paddssw1  33408  pmodlem2  33412  pmodN  33415  pmapjlln1  33420  atmod1i2  33424  pexmidlem2N  33536  pexmidlem7N  33541  pl42lem2N  33545  pl42lem3N  33546  pl42lem4N  33547  pl42N  33548  lhp2lt  33566  lhpm0atN  33594  lautlt  33656  lautcvr  33657  lautj  33658  lautm  33659  ltrneq2  33713  cdleme1b  33792  cdleme3b  33795  cdleme3c  33796  cdleme9b  33818  cdlemefs27cl  33980  cdleme42mN  34054  cdlemg4c  34179  trljco  34307  tgrpgrplem  34316  tendoplass  34350  tendodi1  34351  tendodi2  34352  erngplus2  34371  erngplus2-rN  34379  cdlemk36  34480  erngdvlem3  34557  erngdvlem3-rN  34565  dvaplusgv  34577  tendospass  34587  tendospdi1  34588  dvalveclem  34593  dialss  34614  dvhvaddass  34665  dvhopvsca  34670  dvhlveclem  34676  diblss  34738  diclss  34761  diclspsn  34762  cdlemn11pre  34778  dihmeetlem12N  34886  dihmeetlem16N  34890  dihmeetlem17N  34891  dvh4dimN  35015  lpolsatN  35056  lpolpolsatN  35057  dochpolN  35058  lclkr  35101  lclkrs  35107  lcfr  35153  irrapxlem6  35671  jm2.26lem3  35856  mpaamn  36022  mendring  36058  mendlmod  36059  mendassa  36060  rfcnpre4  37355  fmuldfeq  37661  stoweidlem43  37904  stoweidlem52  37913  stoweidlem53  37914  stoweidlem56  37917  iccelpart  38747  pfxccat3a  38970  funopsn  39018  structiedg0val  39124  subgruhgredgd  39356  upgrspths1wlk  39697  copissgrp  39861  ringrng  39932  cznrng  40010  funcringcsetcALTV2lem9  40099  funcringcsetclem9ALTV  40122  linccl  40260  lincsumscmcl  40279  ldepsprlem  40318  lincresunit3lem1  40325
  Copyright terms: Public domain W3C validator