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

Theorem simprll 738
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 443 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 708 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  disjxiun  4020  fcof1  5797  mpt20  6199  eroveu  6753  boxriin  6858  undom  6950  fofinf1o  7137  finsschain  7162  marypha1lem  7186  wemapso2lem  7265  wemapso  7266  wemapso2  7267  cantnf  7395  iunfictbso  7741  enfin2i  7947  ttukeylem7  8142  fpwwe2lem2  8254  fpwwe2lem9  8260  fpwwe2lem12  8263  fpwwelem  8267  distrlem4pr  8650  divdivdiv  9461  divmuleq  9465  divadddiv  9475  divsubdiv  9476  lediv12a  9649  xmullem  10584  xlemul1a  10608  seqcaopr  11083  leexp2r  11159  hashf1lem1  11393  hashf1lem2  11394  lo1le  12125  summolem2  12189  summo  12190  bezoutlem3  12719  bezoutlem4  12720  qredeu  12786  pcadd  12937  prmreclem2  12964  vdwlem9  13036  vdwlem10  13037  ramub1lem2  13074  ramub1  13075  cofucl  13762  setcmon  13919  poslubmo  14250  grprcan  14515  isnsg3  14651  ghmpreima  14704  gaorber  14762  odcau  14915  lsmsubm  14964  lsmmod  14984  ablfaclem3  15322  rngpropd  15372  lmodprop2d  15687  lss1d  15720  mplcoe1  16209  mplcoe2  16211  ppttop  16744  epttop  16746  cnhaus  17082  isreg2  17105  cncmp  17119  1stcfb  17171  2ndcomap  17184  1stccnp  17188  cldllycmp  17221  1stckgenlem  17248  txcls  17299  ptcnp  17316  txdis1cn  17329  txlly  17330  txnlly  17331  pthaus  17332  txhaus  17341  txkgen  17346  xkohaus  17347  xkococnlem  17353  xkococn  17354  opnfbas  17537  hausflimi  17675  hausflim  17676  hauspwpwf1  17682  alexsubALT  17745  tgpconcomp  17795  divstgplem  17803  metequiv2  18056  met2ndci  18068  nrmmetd  18097  nlmvscnlem1  18197  reconn  18333  xrge0tsms  18339  mulc1cncf  18409  ipcnlem1  18672  minveclem3  18793  pmltpc  18810  ovolicc2lem5  18880  ovolicc2  18881  uniioombllem6  18943  dyadmbllem  18954  vitalilem3  18965  mbfmullem  19080  itg2split  19104  itg2mono  19108  dvlip2  19342  lhop1  19361  dvcnvrelem1  19364  dvfsumrlim  19378  ftc1lem6  19388  itgsubst  19396  evlslem1  19399  dgrco  19656  plyexmo  19693  ulmdvlem3  19779  abelthlem2  19808  abelthlem8  19815  dvdsmulf1o  20434  chpchtsum  20458  dchrptlem2  20504  2sqlem5  20607  2sqlem9  20612  2sqb  20617  chpo1ubb  20630  vmadivsumb  20632  selbergb  20698  selberg2b  20701  selberg3lem2  20707  pntrsumbnd  20715  pntrlog2bnd  20733  pntibndlem3  20741  pnt3  20761  ablo4  20954  ghgrp  21035  smcnlem  21270  pjhthmo  21881  pjpjpre  21998  lnconi  22613  xrge0tsmsd  23382  derangenlem  23702  pconcon  23762  conpcon  23766  cvmfolem  23810  cvmliftmolem2  23813  cvmliftmo  23815  cvmliftlem7  23822  cvmlift2lem10  23843  cvmlift3lem8  23857  dedekind  24082  axsegcon  24555  ax5seglem9  24565  axeuclid  24591  axcontlem10  24601  axcontlem12  24603  linecgr  24704  btwnconn1lem8  24717  btwnconn1lem14  24723  btwnconn3  24726  brsegle  24731  segletr  24737  segleantisym  24738  outsideofeq  24753  linethru  24776  resgcom  25351  fprodsub  25379  iintlem1  25610  icccon3  25701  finminlem  26231  nn0prpwlem  26238  neibastop2lem  26309  isbnd3  26508  mzpcl1  26807  mzpcompact2lem  26829  diophin  26852  pell14qrmulcl  26948  pwssplit4  27191  lindff1  27290  islindf4  27308  hbtlem2  27328  issubmd  27383  psgneu  27429  stoweidlem57  27806  stoweidlem61  27810  cvlcvr1  29529  athgt  29645  4atlem12  29801  paddasslem12  30020  paddasslem13  30021  cdleme0cp  30403  cdleme42keg  30675  cdleme42mgN  30677  trlord  30758  cdlemg6c  30809  cdlemkid4  31123  dihopelvalcpre  31438  dihmeetlem1N  31480  dihglblem5apreN  31481  dihmeetlem4preN  31496  dihmeetlem6  31499  dihmeetlem10N  31506  dihmeetlem11N  31507  dihmeetlem13N  31509  dihjatcclem4  31611
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 177  df-an 360
  Copyright terms: Public domain W3C validator