MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprll Structured version   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  4209  fcof1  6020  mpt20  6427  eroveu  6999  boxriin  7104  undom  7196  fofinf1o  7387  finsschain  7413  marypha1lem  7438  wemapso2lem  7519  wemapso  7520  wemapso2  7521  cantnf  7649  iunfictbso  7995  enfin2i  8201  ttukeylem7  8395  fpwwe2lem2  8507  fpwwe2lem9  8513  fpwwe2lem12  8516  fpwwelem  8520  distrlem4pr  8903  divdivdiv  9715  divmuleq  9719  divadddiv  9729  divsubdiv  9730  lediv12a  9903  xmullem  10843  xlemul1a  10867  seqcaopr  11360  leexp2r  11437  hashf1lem1  11704  hashf1lem2  11705  lo1le  12445  summolem2  12510  summo  12511  bezoutlem3  13040  bezoutlem4  13041  qredeu  13107  pcadd  13258  prmreclem2  13285  vdwlem9  13357  vdwlem10  13358  ramub1lem2  13395  ramub1  13396  cofucl  14085  setcmon  14242  poslubmo  14573  grprcan  14838  isnsg3  14974  ghmpreima  15027  gaorber  15085  odcau  15238  lsmsubm  15287  lsmmod  15307  ablfaclem3  15645  rngpropd  15695  lmodprop2d  16006  lss1d  16039  mplcoe1  16528  mplcoe2  16530  ppttop  17071  epttop  17073  cnhaus  17418  isreg2  17441  cncmp  17455  1stcfb  17508  2ndcomap  17521  1stccnp  17525  cldllycmp  17558  1stckgenlem  17585  txcls  17636  ptcnp  17654  txdis1cn  17667  txlly  17668  txnlly  17669  pthaus  17670  txhaus  17679  txkgen  17684  xkohaus  17685  xkococnlem  17691  xkococn  17692  opnfbas  17874  hausflimi  18012  hausflim  18013  hauspwpwf1  18019  alexsubALT  18082  tgpconcomp  18142  divstgplem  18150  metequiv2  18540  met2ndci  18552  nrmmetd  18622  nlmvscnlem1  18722  reconn  18859  xrge0tsms  18865  mulc1cncf  18935  ipcnlem1  19199  minveclem3  19330  pmltpc  19347  ovolicc2lem5  19417  ovolicc2  19418  uniioombllem6  19480  dyadmbllem  19491  vitalilem3  19502  mbfmullem  19617  itg2split  19641  itg2mono  19645  dvlip2  19879  lhop1  19898  dvcnvrelem1  19901  dvfsumrlim  19915  ftc1lem6  19925  itgsubst  19933  evlslem1  19936  dgrco  20193  plyexmo  20230  ulmdvlem3  20318  abelthlem2  20348  abelthlem8  20355  dvdsmulf1o  20979  chpchtsum  21003  dchrptlem2  21049  2sqlem5  21152  2sqlem9  21157  2sqb  21162  chpo1ubb  21175  vmadivsumb  21177  selbergb  21243  selberg2b  21246  selberg3lem2  21252  pntrsumbnd  21260  pntrlog2bnd  21278  pntibndlem3  21286  pnt3  21306  ablo4  21875  ghgrp  21956  smcnlem  22193  pjhthmo  22804  pjpjpre  22921  lnconi  23536  xrge0tsmsd  24223  derangenlem  24857  pconcon  24918  conpcon  24922  cvmfolem  24966  cvmliftmolem2  24969  cvmliftmo  24971  cvmliftlem7  24978  cvmlift2lem10  24999  cvmlift3lem8  25013  dedekind  25187  prodmolem2  25261  prodmo  25262  axsegcon  25866  ax5seglem9  25876  axeuclid  25902  axcontlem10  25912  axcontlem12  25914  linecgr  26015  btwnconn1lem8  26028  btwnconn1lem14  26034  btwnconn3  26037  brsegle  26042  segletr  26048  segleantisym  26049  outsideofeq  26064  linethru  26087  mblfinlem3  26245  bddiblnc  26275  ftc1cnnc  26279  finminlem  26321  nn0prpwlem  26325  neibastop2lem  26389  isbnd3  26493  mzpcl1  26786  mzpcompact2lem  26808  diophin  26831  pell14qrmulcl  26926  pwssplit4  27168  lindff1  27267  islindf4  27285  hbtlem2  27305  issubmd  27360  psgneu  27406  stoweidlem57  27782  stoweidlem61  27786  cvlcvr1  30137  athgt  30253  4atlem12  30409  paddasslem12  30628  paddasslem13  30629  cdleme0cp  31011  cdleme42keg  31283  cdleme42mgN  31285  trlord  31366  cdlemg6c  31417  cdlemkid4  31731  dihopelvalcpre  32046  dihmeetlem1N  32088  dihglblem5apreN  32089  dihmeetlem4preN  32104  dihmeetlem6  32107  dihmeetlem10N  32114  dihmeetlem11N  32115  dihmeetlem13N  32117  dihjatcclem4  32219
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