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

Theorem simprll 739
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 444 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 709 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  disjxiun  4201  fcof1  6011  mpt20  6418  eroveu  6990  boxriin  7095  undom  7187  fofinf1o  7378  finsschain  7404  marypha1lem  7429  wemapso2lem  7508  wemapso  7509  wemapso2  7510  cantnf  7638  iunfictbso  7984  enfin2i  8190  ttukeylem7  8384  fpwwe2lem2  8496  fpwwe2lem9  8502  fpwwe2lem12  8505  fpwwelem  8509  distrlem4pr  8892  divdivdiv  9704  divmuleq  9708  divadddiv  9718  divsubdiv  9719  lediv12a  9892  xmullem  10832  xlemul1a  10856  seqcaopr  11348  leexp2r  11425  hashf1lem1  11692  hashf1lem2  11693  lo1le  12433  summolem2  12498  summo  12499  bezoutlem3  13028  bezoutlem4  13029  qredeu  13095  pcadd  13246  prmreclem2  13273  vdwlem9  13345  vdwlem10  13346  ramub1lem2  13383  ramub1  13384  cofucl  14073  setcmon  14230  poslubmo  14561  grprcan  14826  isnsg3  14962  ghmpreima  15015  gaorber  15073  odcau  15226  lsmsubm  15275  lsmmod  15295  ablfaclem3  15633  rngpropd  15683  lmodprop2d  15994  lss1d  16027  mplcoe1  16516  mplcoe2  16518  ppttop  17059  epttop  17061  cnhaus  17406  isreg2  17429  cncmp  17443  1stcfb  17496  2ndcomap  17509  1stccnp  17513  cldllycmp  17546  1stckgenlem  17573  txcls  17624  ptcnp  17642  txdis1cn  17655  txlly  17656  txnlly  17657  pthaus  17658  txhaus  17667  txkgen  17672  xkohaus  17673  xkococnlem  17679  xkococn  17680  opnfbas  17862  hausflimi  18000  hausflim  18001  hauspwpwf1  18007  alexsubALT  18070  tgpconcomp  18130  divstgplem  18138  metequiv2  18528  met2ndci  18540  nrmmetd  18610  nlmvscnlem1  18710  reconn  18847  xrge0tsms  18853  mulc1cncf  18923  ipcnlem1  19187  minveclem3  19318  pmltpc  19335  ovolicc2lem5  19405  ovolicc2  19406  uniioombllem6  19468  dyadmbllem  19479  vitalilem3  19490  mbfmullem  19605  itg2split  19629  itg2mono  19633  dvlip2  19867  lhop1  19886  dvcnvrelem1  19889  dvfsumrlim  19903  ftc1lem6  19913  itgsubst  19921  evlslem1  19924  dgrco  20181  plyexmo  20218  ulmdvlem3  20306  abelthlem2  20336  abelthlem8  20343  dvdsmulf1o  20967  chpchtsum  20991  dchrptlem2  21037  2sqlem5  21140  2sqlem9  21145  2sqb  21150  chpo1ubb  21163  vmadivsumb  21165  selbergb  21231  selberg2b  21234  selberg3lem2  21240  pntrsumbnd  21248  pntrlog2bnd  21266  pntibndlem3  21274  pnt3  21294  ablo4  21863  ghgrp  21944  smcnlem  22181  pjhthmo  22792  pjpjpre  22909  lnconi  23524  xrge0tsmsd  24211  derangenlem  24845  pconcon  24906  conpcon  24910  cvmfolem  24954  cvmliftmolem2  24957  cvmliftmo  24959  cvmliftlem7  24966  cvmlift2lem10  24987  cvmlift3lem8  25001  dedekind  25175  prodmolem2  25250  prodmo  25251  axsegcon  25814  ax5seglem9  25824  axeuclid  25850  axcontlem10  25860  axcontlem12  25862  linecgr  25963  btwnconn1lem8  25976  btwnconn1lem14  25982  btwnconn3  25985  brsegle  25990  segletr  25996  segleantisym  25997  outsideofeq  26012  linethru  26035  mblfinlem2  26191  bddiblnc  26221  ftc1cnnc  26225  finminlem  26258  nn0prpwlem  26262  neibastop2lem  26326  isbnd3  26430  mzpcl1  26723  mzpcompact2lem  26745  diophin  26768  pell14qrmulcl  26863  pwssplit4  27106  lindff1  27205  islindf4  27223  hbtlem2  27243  issubmd  27298  psgneu  27344  stoweidlem57  27720  stoweidlem61  27724  shwrdsdisj  28173  cvlcvr1  29976  athgt  30092  4atlem12  30248  paddasslem12  30467  paddasslem13  30468  cdleme0cp  30850  cdleme42keg  31122  cdleme42mgN  31124  trlord  31205  cdlemg6c  31256  cdlemkid4  31570  dihopelvalcpre  31885  dihmeetlem1N  31927  dihglblem5apreN  31928  dihmeetlem4preN  31943  dihmeetlem6  31946  dihmeetlem10N  31953  dihmeetlem11N  31954  dihmeetlem13N  31956  dihjatcclem4  32058
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
  Copyright terms: Public domain W3C validator