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

Theorem simpr3 965
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 959 . 2  |-  ( ( ps  /\  ch  /\  th )  ->  th )
21adantl 453 1  |-  ( (
ph  /\  ( ps  /\ 
ch  /\  th )
)  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  simplr3  1001  simprr3  1007  simp1r3  1055  simp2r3  1061  simp3r3  1067  3anandis  1285  fr3nr  4760  isopolem  6065  elfir  7420  intrnfi  7421  fisupcl  7472  cnfcomlem  7656  ackbij1lem15  8114  pwfseqlem4a  8536  pwfseqlem4  8537  xlesubadd  10842  elioc2  10973  elico2  10974  elicc2  10975  fseq1p1m1  11122  ccatswrd  11773  tanadd  12768  dvds2ln  12880  ressress  13526  f1ovscpbl  13751  mreexexlem4d  13872  mreexexd  13873  2oppccomf  13951  fthmon  14124  fuccocl  14161  fucidcl  14162  invfuc  14171  curf2cl  14328  yonedalem4c  14374  yonedalem3  14377  pospo  14430  latjlej1  14494  latnlej2  14500  latmlem1  14510  latledi  14518  latjass  14524  latj12  14525  latj32  14526  latj13  14527  latj31  14528  latjrot  14529  latjjdi  14532  latjjdir  14533  latdisdlem  14615  prdsmndd  14728  imasmnd2  14732  imasmnd  14733  frmdmnd  14804  grpsubadd  14876  grpaddsubass  14878  grpsubsub4  14881  grppnpcan2  14882  grpnpncan  14883  grpnnncan2  14884  mulgnndir  14912  mulgnn0dir  14913  mulgnnass  14918  mulgnn0ass  14919  mulgass  14920  pwsmulg  14932  imasgrp2  14933  imasgrp  14934  issubg2  14959  divsgrp  14995  galcan  15081  gacan  15082  symggrp  15103  oppgmnd  15150  frgp0  15392  cmn32  15430  cmn12  15432  abladdsub  15439  mulgdi  15449  mulgsubdi  15452  dprdss  15587  dprdf1o  15590  dprdsn  15594  dmdprdsplit  15605  pgpfac1lem5  15637  rngi  15676  prdsrngd  15718  imasrng  15725  opprrng  15736  mulgass3  15742  dvrass  15795  subrgunit  15886  issubrg2  15888  abvdiv  15925  lss1  16015  lsssn0  16024  islss3  16035  prdslmodd  16045  islmhm2  16114  lspsolv  16215  lbsextlem4  16233  sralmod  16258  issubassa  16383  sraassa  16384  psrbaglesupp  16433  psrbagcon  16436  psrgrp  16462  psrlmod  16465  psrrng  16474  psrassa  16477  mpllsslem  16499  ipdi  16871  ipsubdir  16873  ipsubdi  16874  ipassr  16877  ipassr2  16878  isphld  16885  ocvlss  16899  iinopn  16975  restopnb  17239  subbascn  17318  nrmsep2  17420  isnrm3  17423  t1sep  17434  regsep2  17440  dnsconst  17442  dfcon2  17482  dislly  17560  tx1stc  17682  qtophmeo  17849  filss  17885  infil  17895  fsubbas  17899  filssufilg  17943  hauspwpwf1  18019  cnextcn  18098  tmdcn2  18119  psmettri  18342  isxmet2d  18357  xmettri  18381  xmetres2  18391  bldisj  18428  blss2ps  18433  blss2  18434  xmstri2  18496  mstri2  18497  xmstri  18498  mstri  18499  xmstri3  18500  mstri3  18501  msrtri  18502  comet  18543  met2ndci  18552  ngprcan  18656  ngplcan  18657  ngpsubcan  18660  nrgdsdi  18701  nrgdsdir  18702  nlmdsdi  18717  nlmdsdir  18718  blcvx  18829  iocopnst  18965  icccvx  18975  pi1grplem  19074  pi1xfrf  19078  pi1cof  19084  cphdivcl  19145  cphsubdir  19170  cphsubdi  19171  bcthlem5  19281  volfiniun  19441  volcn  19498  itg1val2  19576  dvconst  19803  dvlip  19877  ftc1a  19921  ulmdvlem3  20318  ang180  20656  cvxcl  20823  scvxcvx  20824  sgmmul  20985  logexprlim  21009  dchrabl  21038  isspthonpth  21584  wlkdvspth  21608  grpomuldivass  21837  grpopnpcan2  21841  grponpncan  21843  grpodiveq  21844  ablodivdiv4  21879  ablonnncan  21881  ismndo1  21932  nvsubadd  22136  dipdi  22344  dipsubdi  22350  disjdsct  24090  dvrdir  24226  dvrcan5  24229  kerf1hrm  24262  reofld  24280  pstmfval  24291  qqhval2lem  24365  qqhvq  24371  esumcvg  24476  sigaclcu  24500  measdivcstOLD  24578  measdivcst  24579  erdszelem9  24885  cvmseu  24963  colinearalglem1  25845  colinearalg  25849  axcgrtr  25854  axlowdimlem16  25896  axeuclidlem  25901  axcontlem4  25906  axcontlem7  25909  axcontlem12  25914  cgrid2  25937  btwncomim  25947  btwnswapid  25951  trisegint  25962  cgrxfr  25989  btwnxfr  25990  brofs2  26011  brifs2  26012  endofsegid  26019  btwnconn1lem11  26031  btwnconn2  26036  segcon2  26039  seglemin  26047  segletr  26048  btwnsegle  26051  colinbtwnle  26052  broutsideof2  26056  btwnoutside  26059  broutsideof3  26060  outsideoftr  26063  outsidele  26066  ellines  26086  linethrueu  26090  ftc1anc  26288  sdclem1  26447  sstotbnd2  26483  zerdivemp1x  26571  isdrngo2  26574  iscringd  26609  irrapxlem6  26890  jm2.26lem3  27072  mpaamn  27338  pmtrprfv  27373  psgnunilem3  27396  matrng  27457  matassa  27458  mendrng  27477  mendlmod  27478  mendassa  27479  rfcnpre4  27681  fmuldfeq  27689  stoweidlem43  27768  stoweidlem52  27777  stoweidlem53  27778  stoweidlem56  27781  swdeq  28196  swrdccatin2lem1  28206  usg2wotspth  28351  2pthwlkonot  28352  bnj970  29318  bnj910  29319  lsmsat  29806  lfladdcl  29869  lflnegcl  29873  lflvscl  29875  lshpkrlem4  29911  lshpkrlem6  29913  ldualgrplem  29943  lduallmodlem  29950  latmassOLD  30027  latm12  30028  latm32  30029  latmrot  30030  latmmdiN  30032  latmmdir  30033  omlfh1N  30056  omlfh3N  30057  cvrnbtwn2  30073  cvlexchb1  30128  cvlexch3  30130  cvlexch4N  30131  cvlatexchb1  30132  cvlsupr2  30141  hlatjass  30167  hlatj12  30168  hlatj32  30169  cvrat  30219  atcvrj0  30225  cvrat2  30226  atltcvr  30232  atexchltN  30238  cvrat3  30239  cvrat4  30240  atbtwnexOLDN  30244  atbtwnex  30245  3dimlem3  30258  3dimlem3OLDN  30259  3at  30287  2atneat  30312  llncmp  30319  2at0mat0  30322  2atmat0  30323  islpln2a  30345  llncvrlpln  30355  lplncmp  30359  3atnelvolN  30383  4atlem11  30406  lplncvrlvol  30413  lvolcmp  30414  2atm2atN  30582  elpaddatriN  30600  elpadd2at2  30604  paddasslem8  30624  paddasslem17  30633  paddass  30635  padd12N  30636  paddssw1  30640  pmodlem2  30644  pmodN  30647  pmapjlln1  30652  atmod1i2  30656  pexmidlem2N  30768  pexmidlem7N  30773  pl42lem2N  30777  pl42lem3N  30778  pl42lem4N  30779  pl42N  30780  lhp2lt  30798  lhpm0atN  30826  lautlt  30888  lautcvr  30889  lautj  30890  lautm  30891  ltrneq2  30945  cdleme1b  31023  cdleme3b  31026  cdleme3c  31027  cdleme9b  31049  cdlemefs27cl  31210  cdleme42mN  31284  cdlemg4c  31409  trljco  31537  tgrpgrplem  31546  tendoplass  31580  tendodi1  31581  tendodi2  31582  erngplus2  31601  erngplus2-rN  31609  cdlemk36  31710  erngdvlem3  31787  erngdvlem3-rN  31795  dvaplusgv  31807  tendospass  31817  tendospdi1  31818  dvalveclem  31823  dialss  31844  dvhvaddass  31895  dvhopvsca  31900  dvhlveclem  31906  diblss  31968  diclss  31991  diclspsn  31992  cdlemn11pre  32008  dihmeetlem12N  32116  dihmeetlem16N  32120  dihmeetlem17N  32121  dvh4dimN  32245  lpolsatN  32286  lpolpolsatN  32287  dochpolN  32288  lclkr  32331  lclkrs  32337  lcfr  32383
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator