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  4169  fcof1  5979  mpt20  6386  eroveu  6958  boxriin  7063  undom  7155  fofinf1o  7346  finsschain  7371  marypha1lem  7396  wemapso2lem  7475  wemapso  7476  wemapso2  7477  cantnf  7605  iunfictbso  7951  enfin2i  8157  ttukeylem7  8351  fpwwe2lem2  8463  fpwwe2lem9  8469  fpwwe2lem12  8472  fpwwelem  8476  distrlem4pr  8859  divdivdiv  9671  divmuleq  9675  divadddiv  9685  divsubdiv  9686  lediv12a  9859  xmullem  10799  xlemul1a  10823  seqcaopr  11315  leexp2r  11392  hashf1lem1  11659  hashf1lem2  11660  lo1le  12400  summolem2  12465  summo  12466  bezoutlem3  12995  bezoutlem4  12996  qredeu  13062  pcadd  13213  prmreclem2  13240  vdwlem9  13312  vdwlem10  13313  ramub1lem2  13350  ramub1  13351  cofucl  14040  setcmon  14197  poslubmo  14528  grprcan  14793  isnsg3  14929  ghmpreima  14982  gaorber  15040  odcau  15193  lsmsubm  15242  lsmmod  15262  ablfaclem3  15600  rngpropd  15650  lmodprop2d  15961  lss1d  15994  mplcoe1  16483  mplcoe2  16485  ppttop  17026  epttop  17028  cnhaus  17372  isreg2  17395  cncmp  17409  1stcfb  17461  2ndcomap  17474  1stccnp  17478  cldllycmp  17511  1stckgenlem  17538  txcls  17589  ptcnp  17607  txdis1cn  17620  txlly  17621  txnlly  17622  pthaus  17623  txhaus  17632  txkgen  17637  xkohaus  17638  xkococnlem  17644  xkococn  17645  opnfbas  17827  hausflimi  17965  hausflim  17966  hauspwpwf1  17972  alexsubALT  18035  tgpconcomp  18095  divstgplem  18103  metequiv2  18493  met2ndci  18505  nrmmetd  18575  nlmvscnlem1  18675  reconn  18812  xrge0tsms  18818  mulc1cncf  18888  ipcnlem1  19152  minveclem3  19283  pmltpc  19300  ovolicc2lem5  19370  ovolicc2  19371  uniioombllem6  19433  dyadmbllem  19444  vitalilem3  19455  mbfmullem  19570  itg2split  19594  itg2mono  19598  dvlip2  19832  lhop1  19851  dvcnvrelem1  19854  dvfsumrlim  19868  ftc1lem6  19878  itgsubst  19886  evlslem1  19889  dgrco  20146  plyexmo  20183  ulmdvlem3  20271  abelthlem2  20301  abelthlem8  20308  dvdsmulf1o  20932  chpchtsum  20956  dchrptlem2  21002  2sqlem5  21105  2sqlem9  21110  2sqb  21115  chpo1ubb  21128  vmadivsumb  21130  selbergb  21196  selberg2b  21199  selberg3lem2  21205  pntrsumbnd  21213  pntrlog2bnd  21231  pntibndlem3  21239  pnt3  21259  ablo4  21828  ghgrp  21909  smcnlem  22146  pjhthmo  22757  pjpjpre  22874  lnconi  23489  xrge0tsmsd  24176  derangenlem  24810  pconcon  24871  conpcon  24875  cvmfolem  24919  cvmliftmolem2  24922  cvmliftmo  24924  cvmliftlem7  24931  cvmlift2lem10  24952  cvmlift3lem8  24966  dedekind  25140  prodmolem2  25214  prodmo  25215  axsegcon  25770  ax5seglem9  25780  axeuclid  25806  axcontlem10  25816  axcontlem12  25818  linecgr  25919  btwnconn1lem8  25932  btwnconn1lem14  25938  btwnconn3  25941  brsegle  25946  segletr  25952  segleantisym  25953  outsideofeq  25968  linethru  25991  mblfinlem2  26144  bddiblnc  26174  ftc1cnnc  26178  finminlem  26211  nn0prpwlem  26215  neibastop2lem  26279  isbnd3  26383  mzpcl1  26676  mzpcompact2lem  26698  diophin  26721  pell14qrmulcl  26816  pwssplit4  27059  lindff1  27158  islindf4  27176  hbtlem2  27196  issubmd  27251  psgneu  27297  stoweidlem57  27673  stoweidlem61  27677  cvlcvr1  29822  athgt  29938  4atlem12  30094  paddasslem12  30313  paddasslem13  30314  cdleme0cp  30696  cdleme42keg  30968  cdleme42mgN  30970  trlord  31051  cdlemg6c  31102  cdlemkid4  31416  dihopelvalcpre  31731  dihmeetlem1N  31773  dihglblem5apreN  31774  dihmeetlem4preN  31789  dihmeetlem6  31792  dihmeetlem10N  31799  dihmeetlem11N  31800  dihmeetlem13N  31802  dihjatcclem4  31904
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