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

Theorem simprll 761
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprll  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )

Proof of Theorem simprll
StepHypRef Expression
1 simpl 457 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 727 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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
This theorem is referenced by:  disjxiun  4400  fcof1  6103  mpt20  6268  eroveu  7308  boxriin  7418  undom  7512  fofinf1o  7706  finsschain  7732  suppeqfsuppbi  7748  fsuppunbi  7755  marypha1lem  7797  wemapsolem  7878  wemapso  7879  wemapso2OLD  7880  wemapso2lem  7881  cantnf  8015  cantnfOLD  8037  iunfictbso  8398  enfin2i  8604  ttukeylem7  8798  fpwwe2lem2  8913  fpwwe2lem9  8919  fpwwe2lem12  8922  fpwwelem  8926  distrlem4pr  9309  dedekind  9647  divdivdiv  10146  divmuleq  10150  divadddiv  10160  divsubdiv  10161  lediv12a  10339  xmullem  11341  xlemul1a  11365  seqcaopr  11963  leexp2r  12041  hashf1lem1  12329  hashf1lem2  12330  wrd2ind  12493  cshweqrep  12576  lo1le  13250  summolem2  13314  summo  13315  bezoutlem3  13845  bezoutlem4  13846  qredeu  13914  pcadd  14072  prmreclem2  14099  vdwlem9  14171  vdwlem10  14172  ramub1lem2  14209  ramub1  14210  cofucl  14920  setcmon  15077  poslubmo  15438  posglbmo  15439  issubmd  15599  grprcan  15693  isnsg3  15837  ghmpreima  15890  gaorber  15948  psgneu  16134  odcau  16227  lsmsubm  16276  lsmmod  16296  ablfaclem3  16713  rngpropd  16802  lmodprop2d  17133  lss1d  17170  mplcoe1  17671  mplcoe5  17675  mplcoe2OLD  17677  evlslem1  17728  lindff1  18377  islindf4  18395  mdetunilem7  18559  mdetunilem8  18560  mdetunilem9  18561  mdetuni0  18562  mdetmul  18564  ppttop  18746  epttop  18748  cnhaus  19093  isreg2  19116  cncmp  19130  1stcfb  19184  2ndcomap  19197  1stccnp  19201  cldllycmp  19234  1stckgenlem  19261  txcls  19312  ptcnp  19330  txdis1cn  19343  txlly  19344  txnlly  19345  pthaus  19346  txhaus  19355  txkgen  19360  xkohaus  19361  xkococnlem  19367  xkococn  19368  opnfbas  19550  hausflimi  19688  hausflim  19689  hauspwpwf1  19695  alexsubALT  19758  tgpconcomp  19818  divstgplem  19826  metequiv2  20220  met2ndci  20232  nrmmetd  20302  nlmvscnlem1  20402  reconn  20540  xrge0tsms  20546  mulc1cncf  20616  ipcnlem1  20892  minveclem3  21051  pmltpc  21069  ovolicc2lem5  21139  ovolicc2  21140  uniioombllem6  21204  dyadmbllem  21215  vitalilem3  21226  mbfmullem  21339  itg2split  21363  itg2mono  21367  dvlip2  21603  lhop1  21622  dvcnvrelem1  21625  dvfsumrlim  21639  ftc1lem6  21649  itgsubst  21657  dgrco  21878  plyexmo  21915  ulmdvlem3  22003  abelthlem2  22033  abelthlem8  22040  dvdsmulf1o  22670  chpchtsum  22694  dchrptlem2  22740  2sqlem5  22843  2sqlem9  22848  2sqb  22853  chpo1ubb  22866  vmadivsumb  22868  selbergb  22934  selberg2b  22937  selberg3lem2  22943  pntrsumbnd  22951  pntrlog2bnd  22969  pntibndlem3  22977  pnt3  22997  mirreu3  23202  axsegcon  23345  ax5seglem9  23355  axeuclid  23381  axcontlem10  23391  axcontlem12  23393  ablo4  23946  ghgrp  24027  smcnlem  24264  pjhthmo  24877  pjpjpre  24994  lnconi  25609  resf1o  26201  xrge0tsmsd  26418  derangenlem  27223  pconcon  27284  conpcon  27288  cvmfolem  27332  cvmliftmolem2  27335  cvmliftmo  27337  cvmliftlem7  27344  cvmlift2lem10  27365  cvmlift3lem8  27379  prodmolem2  27612  prodmo  27613  linecgr  28276  btwnconn1lem8  28289  btwnconn1lem14  28295  btwnconn3  28298  brsegle  28303  segletr  28309  segleantisym  28310  outsideofeq  28325  linethru  28348  mblfinlem3  28598  bddiblnc  28630  ftc1cnnc  28634  finminlem  28681  nn0prpwlem  28685  neibastop2lem  28749  isbnd3  28851  mzpcl1  29233  mzpcompact2lem  29256  diophin  29279  pell14qrmulcl  29372  pwssplit4  29610  hbtlem2  29648  stoweidlem57  30020  stoweidlem61  30024  wwlknredwwlkn0  30527  clwwlkextfrlem1  30837  numclwlk1lem2f1  30855  numclwlk1lem2fo  30856  lmodvsmdi  30987  lmodvsmmulgdi  30988  assamulgscmlem2  30996  cayhamlem3  31394  cvlcvr1  33342  athgt  33458  4atlem12  33614  paddasslem12  33833  paddasslem13  33834  cdleme0cp  34216  cdleme42keg  34488  cdleme42mgN  34490  trlord  34571  cdlemg6c  34622  cdlemkid4  34936  dihopelvalcpre  35251  dihmeetlem1N  35293  dihglblem5apreN  35294  dihmeetlem4preN  35309  dihmeetlem6  35312  dihmeetlem10N  35319  dihmeetlem11N  35320  dihmeetlem13N  35322  dihjatcclem4  35424
  Copyright terms: Public domain W3C validator