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

Theorem simprll 766
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 457 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 728 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 187  df-an 371
This theorem is referenced by:  disjxiun  4394  fcof1  6175  mpt20  6350  wfrlem17  7039  eroveu  7445  boxriin  7551  undom  7645  fofinf1o  7837  finsschain  7863  suppeqfsuppbi  7879  fsuppunbi  7886  marypha1lem  7929  wemapsolem  8011  wemapso  8012  wemapso2OLD  8013  wemapso2lem  8014  cantnf  8146  cantnfOLD  8168  iunfictbso  8529  enfin2i  8735  ttukeylem7  8929  fpwwe2lem2  9042  fpwwe2lem9  9048  fpwwe2lem12  9051  fpwwelem  9055  distrlem4pr  9436  mulcmpblnr  9480  prsrlem1  9481  dedekind  9780  divdivdiv  10288  divmuleq  10292  divadddiv  10302  divsubdiv  10303  lediv12a  10480  xmullem  11511  xlemul1a  11535  seqcaopr  12190  leexp2r  12270  hashf1lem1  12555  hashf1lem2  12556  wrd2ind  12761  cshweqrep  12847  lo1le  13625  summolem2  13689  summo  13690  prodmolem2  13896  prodmo  13897  bezoutlem3  14389  bezoutlem4  14390  qredeu  14459  pcadd  14619  prmreclem2  14646  vdwlem9  14718  vdwlem10  14719  ramub1lem2  14756  ramub1  14757  cofucl  15503  setcmon  15692  poslubmo  16102  posglbmo  16103  issubmd  16306  grprcan  16409  isnsg3  16561  ghmpreima  16614  gaorber  16672  psgneu  16857  odcau  16950  lsmsubm  16999  lsmmod  17019  ablfaclem3  17460  ringpropd  17552  lmodvsmmulgdi  17869  lmodprop2d  17894  lss1d  17931  assamulgscmlem2  18320  mplcoe1  18449  mplcoe5  18453  mplcoe2OLD  18455  evlslem1  18506  lindff1  19149  islindf4  19167  mdetunilem7  19414  mdetunilem8  19415  mdetunilem9  19416  mdetuni0  19417  mdetmul  19419  cayhamlem3  19682  ppttop  19802  epttop  19804  cnhaus  20150  isreg2  20173  cncmp  20187  1stcfb  20240  2ndcomap  20253  1stccnp  20257  cldllycmp  20290  1stckgenlem  20348  txcls  20399  ptcnp  20417  txdis1cn  20430  txlly  20431  txnlly  20432  pthaus  20433  txhaus  20442  txkgen  20447  xkohaus  20448  xkococnlem  20454  xkococn  20455  opnfbas  20637  hausflimi  20775  hausflim  20776  hauspwpwf1  20782  alexsubALT  20845  tgpconcomp  20905  qustgplem  20913  metequiv2  21307  met2ndci  21319  nrmmetd  21389  nlmvscnlem1  21489  reconn  21627  xrge0tsms  21633  mulc1cncf  21703  ipcnlem1  21979  minveclem3  22138  pmltpc  22156  ovolicc2lem5  22226  ovolicc2  22227  uniioombllem6  22291  dyadmbllem  22302  vitalilem3  22313  mbfmullem  22426  itg2split  22450  itg2mono  22454  dvlip2  22690  lhop1  22709  dvcnvrelem1  22712  dvfsumrlim  22726  ftc1lem6  22736  itgsubst  22744  dgrco  22966  plyexmo  23003  ulmdvlem3  23091  abelthlem2  23121  abelthlem8  23128  dvdsmulf1o  23853  chpchtsum  23877  dchrptlem2  23923  2sqlem5  24026  2sqlem9  24031  2sqb  24036  chpo1ubb  24049  vmadivsumb  24051  selbergb  24117  selberg2b  24120  selberg3lem2  24126  pntrsumbnd  24134  pntrlog2bnd  24152  pntibndlem3  24160  pnt3  24180  hlcgreu  24387  mirreu3  24424  cgraswap  24581  cgracom  24583  cgratr  24584  acopyeu  24591  axsegcon  24659  ax5seglem9  24669  axeuclid  24695  axcontlem10  24705  axcontlem12  24707  wwlknredwwlkn0  25156  clwwlkextfrlem1  25505  numclwlk1lem2f1  25523  numclwlk1lem2fo  25524  ablo4  25716  ghgrpOLD  25797  smcnlem  26034  pjhthmo  26647  pjpjpre  26764  lnconi  27378  resf1o  28013  xrge0tsmsd  28241  derangenlem  29481  pconcon  29541  conpcon  29545  cvmfolem  29589  cvmliftmolem2  29592  cvmliftmo  29594  cvmliftlem7  29601  cvmlift2lem10  29622  cvmlift3lem8  29636  linecgr  30432  btwnconn1lem8  30445  btwnconn1lem14  30451  btwnconn3  30454  brsegle  30459  segletr  30465  segleantisym  30466  outsideofeq  30481  linethru  30504  finminlem  30559  nn0prpwlem  30563  neibastop2lem  30601  mblfinlem3  31438  bddiblnc  31471  ftc1cnnc  31475  isbnd3  31575  cvlcvr1  32370  athgt  32486  4atlem12  32642  paddasslem12  32861  paddasslem13  32862  cdleme0cp  33245  cdleme42keg  33518  cdleme42mgN  33520  trlord  33601  cdlemg6c  33652  cdlemkid4  33966  dihopelvalcpre  34281  dihmeetlem1N  34323  dihglblem5apreN  34324  dihmeetlem4preN  34339  dihmeetlem6  34342  dihmeetlem10N  34349  dihmeetlem11N  34350  dihmeetlem13N  34352  dihjatcclem4  34454  mzpcl1  35036  mzpcompact2lem  35058  diophin  35080  pell14qrmulcl  35173  pwssplit4  35410  hbtlem2  35450  iunrelexpuztr  35711  stoweidlem57  37220  stoweidlem61  37224  fourierdlem92  37362  rabsubmgmd  38121  2zlidl  38264  lmodvsmdi  38499
  Copyright terms: Public domain W3C validator