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

Theorem simprll 772
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 459 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 734 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  disjxiun  4399  fcof1  6185  mpt20  6361  wfrlem17  7052  eroveu  7458  boxriin  7564  undom  7660  fofinf1o  7852  finsschain  7881  suppeqfsuppbi  7897  fsuppunbi  7904  marypha1lem  7947  wemapsolem  8065  wemapso  8066  wemapso2lem  8067  cantnf  8198  iunfictbso  8545  enfin2i  8751  ttukeylem7  8945  fpwwe2lem2  9057  fpwwe2lem9  9063  fpwwe2lem12  9066  fpwwelem  9070  distrlem4pr  9451  mulcmpblnr  9495  prsrlem1  9496  dedekind  9797  divdivdiv  10308  divmuleq  10312  divadddiv  10322  divsubdiv  10323  lediv12a  10499  xmullem  11550  xlemul1a  11574  seqcaopr  12250  leexp2r  12330  hashf1lem1  12618  hashf1lem2  12619  wrd2ind  12834  cshweqrep  12920  lo1le  13715  summolem2  13782  summo  13783  prodmolem2  13989  prodmo  13990  bezoutlem3OLD  14505  bezoutlem4OLD  14506  bezoutlem3  14508  bezoutlem4  14509  qredeu  14664  pcadd  14834  prmreclem2  14861  vdwlem9  14939  vdwlem10  14940  ramub1lem2  14985  ramub1  14986  prmgaplem7  15027  cofucl  15793  setcmon  15982  poslubmo  16392  posglbmo  16393  issubmd  16596  grprcan  16699  isnsg3  16851  ghmpreima  16904  gaorber  16962  psgneu  17147  odcau  17256  lsmsubm  17305  lsmmod  17325  ablfaclem3  17720  ringpropd  17812  lmodvsmmulgdi  18126  lmodprop2d  18150  lss1d  18186  assamulgscmlem2  18573  mplcoe1  18689  mplcoe5  18692  evlslem1  18738  lindff1  19378  islindf4  19396  mdetunilem7  19643  mdetunilem8  19644  mdetunilem9  19645  mdetuni0  19646  mdetmul  19648  cayhamlem3  19911  ppttop  20022  epttop  20024  cnhaus  20370  isreg2  20393  cncmp  20407  1stcfb  20460  2ndcomap  20473  1stccnp  20477  cldllycmp  20510  1stckgenlem  20568  txcls  20619  ptcnp  20637  txdis1cn  20650  txlly  20651  txnlly  20652  pthaus  20653  txhaus  20662  txkgen  20667  xkohaus  20668  xkococnlem  20674  xkococn  20675  opnfbas  20857  hausflimi  20995  hausflim  20996  hauspwpwf1  21002  alexsubALT  21066  tgpconcomp  21127  qustgplem  21135  metequiv2  21525  met2ndci  21537  nrmmetd  21589  nlmvscnlem1  21689  reconn  21846  xrge0tsms  21852  mulc1cncf  21937  ipcnlem1  22216  minveclem3  22371  minveclem3OLD  22383  pmltpc  22401  ovolicc2lem5  22475  ovolicc2  22476  uniioombllem6  22546  dyadmbllem  22557  vitalilem3  22568  mbfmullem  22683  itg2split  22707  itg2mono  22711  dvlip2  22947  lhop1  22966  dvcnvrelem1  22969  dvfsumrlim  22983  ftc1lem6  22993  itgsubst  23001  dgrco  23229  plyexmo  23266  ulmdvlem3  23357  abelthlem2  23387  abelthlem8  23394  dvdsmulf1o  24123  chpchtsum  24147  dchrptlem2  24193  2sqlem5  24296  2sqlem9  24301  2sqb  24306  chpo1ubb  24319  vmadivsumb  24321  selbergb  24387  selberg2b  24390  selberg3lem2  24396  pntrsumbnd  24404  pntrlog2bnd  24422  pntibndlem3  24430  pnt3  24450  hlcgreu  24663  mirreu3  24699  cgraswap  24862  cgracom  24864  cgratr  24865  acopyeu  24875  axsegcon  24957  ax5seglem9  24967  axeuclid  24993  axcontlem10  25003  axcontlem12  25005  wwlknredwwlkn0  25455  clwwlkextfrlem1  25804  numclwlk1lem2f1  25822  numclwlk1lem2fo  25823  ablo4  26015  ghgrpOLD  26096  smcnlem  26333  pjhthmo  26955  pjpjpre  27072  lnconi  27686  resf1o  28315  xrge0tsmsd  28548  derangenlem  29894  pconcon  29954  conpcon  29958  cvmfolem  30002  cvmliftmolem2  30005  cvmliftmo  30007  cvmliftlem7  30014  cvmlift2lem10  30035  cvmlift3lem8  30049  linecgr  30848  btwnconn1lem8  30861  btwnconn1lem14  30867  btwnconn3  30870  brsegle  30875  segletr  30881  segleantisym  30882  outsideofeq  30897  linethru  30920  finminlem  30974  nn0prpwlem  30978  neibastop2lem  31016  mblfinlem3  31979  bddiblnc  32012  ftc1cnnc  32016  isbnd3  32116  cvlcvr1  32905  athgt  33021  4atlem12  33177  paddasslem12  33396  paddasslem13  33397  cdleme0cp  33780  cdleme42keg  34053  cdleme42mgN  34055  trlord  34136  cdlemg6c  34187  cdlemkid4  34501  dihopelvalcpre  34816  dihmeetlem1N  34858  dihglblem5apreN  34859  dihmeetlem4preN  34874  dihmeetlem6  34877  dihmeetlem10N  34884  dihmeetlem11N  34885  dihmeetlem13N  34887  dihjatcclem4  34989  mzpcl1  35571  mzpcompact2lem  35593  diophin  35615  pell14qrmulcl  35709  pwssplit4  35947  hbtlem2  35983  iunrelexpuztr  36311  stoweidlem57  37918  stoweidlem61  37922  fourierdlem92  38062  rabsubmgmd  39844  2zlidl  39987  lmodvsmdi  40220
  Copyright terms: Public domain W3C validator