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  4150  fcof1  5959  mpt20  6366  eroveu  6935  boxriin  7040  undom  7132  fofinf1o  7323  finsschain  7348  marypha1lem  7373  wemapso2lem  7452  wemapso  7453  wemapso2  7454  cantnf  7582  iunfictbso  7928  enfin2i  8134  ttukeylem7  8328  fpwwe2lem2  8440  fpwwe2lem9  8446  fpwwe2lem12  8449  fpwwelem  8453  distrlem4pr  8836  divdivdiv  9647  divmuleq  9651  divadddiv  9661  divsubdiv  9662  lediv12a  9835  xmullem  10775  xlemul1a  10799  seqcaopr  11287  leexp2r  11364  hashf1lem1  11631  hashf1lem2  11632  lo1le  12372  summolem2  12437  summo  12438  bezoutlem3  12967  bezoutlem4  12968  qredeu  13034  pcadd  13185  prmreclem2  13212  vdwlem9  13284  vdwlem10  13285  ramub1lem2  13322  ramub1  13323  cofucl  14012  setcmon  14169  poslubmo  14500  grprcan  14765  isnsg3  14901  ghmpreima  14954  gaorber  15012  odcau  15165  lsmsubm  15214  lsmmod  15234  ablfaclem3  15572  rngpropd  15622  lmodprop2d  15933  lss1d  15966  mplcoe1  16455  mplcoe2  16457  ppttop  16994  epttop  16996  cnhaus  17340  isreg2  17363  cncmp  17377  1stcfb  17429  2ndcomap  17442  1stccnp  17446  cldllycmp  17479  1stckgenlem  17506  txcls  17557  ptcnp  17575  txdis1cn  17588  txlly  17589  txnlly  17590  pthaus  17591  txhaus  17600  txkgen  17605  xkohaus  17606  xkococnlem  17612  xkococn  17613  opnfbas  17795  hausflimi  17933  hausflim  17934  hauspwpwf1  17940  alexsubALT  18003  tgpconcomp  18063  divstgplem  18071  metequiv2  18430  met2ndci  18442  nrmmetd  18493  nlmvscnlem1  18593  reconn  18730  xrge0tsms  18736  mulc1cncf  18806  ipcnlem1  19070  minveclem3  19197  pmltpc  19214  ovolicc2lem5  19284  ovolicc2  19285  uniioombllem6  19347  dyadmbllem  19358  vitalilem3  19369  mbfmullem  19484  itg2split  19508  itg2mono  19512  dvlip2  19746  lhop1  19765  dvcnvrelem1  19768  dvfsumrlim  19782  ftc1lem6  19792  itgsubst  19800  evlslem1  19803  dgrco  20060  plyexmo  20097  ulmdvlem3  20185  abelthlem2  20215  abelthlem8  20222  dvdsmulf1o  20846  chpchtsum  20870  dchrptlem2  20916  2sqlem5  21019  2sqlem9  21024  2sqb  21029  chpo1ubb  21042  vmadivsumb  21044  selbergb  21110  selberg2b  21113  selberg3lem2  21119  pntrsumbnd  21127  pntrlog2bnd  21145  pntibndlem3  21153  pnt3  21173  ablo4  21723  ghgrp  21804  smcnlem  22041  pjhthmo  22652  pjpjpre  22769  lnconi  23384  xrge0tsmsd  24052  derangenlem  24636  pconcon  24697  conpcon  24701  cvmfolem  24745  cvmliftmolem2  24748  cvmliftmo  24750  cvmliftlem7  24757  cvmlift2lem10  24778  cvmlift3lem8  24792  dedekind  24966  prodmolem2  25040  prodmo  25041  axsegcon  25580  ax5seglem9  25590  axeuclid  25616  axcontlem10  25626  axcontlem12  25628  linecgr  25729  btwnconn1lem8  25742  btwnconn1lem14  25748  btwnconn3  25751  brsegle  25756  segletr  25762  segleantisym  25763  outsideofeq  25778  linethru  25801  bddiblnc  25975  ftc1cnnc  25979  finminlem  26012  nn0prpwlem  26016  neibastop2lem  26080  isbnd3  26184  mzpcl1  26477  mzpcompact2lem  26499  diophin  26522  pell14qrmulcl  26617  pwssplit4  26860  lindff1  26959  islindf4  26977  hbtlem2  26997  issubmd  27052  psgneu  27098  stoweidlem57  27474  stoweidlem61  27478  cvlcvr1  29454  athgt  29570  4atlem12  29726  paddasslem12  29945  paddasslem13  29946  cdleme0cp  30328  cdleme42keg  30600  cdleme42mgN  30602  trlord  30683  cdlemg6c  30734  cdlemkid4  31048  dihopelvalcpre  31363  dihmeetlem1N  31405  dihglblem5apreN  31406  dihmeetlem4preN  31421  dihmeetlem6  31424  dihmeetlem10N  31431  dihmeetlem11N  31432  dihmeetlem13N  31434  dihjatcclem4  31536
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