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

Theorem simprll 780
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 464 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 742 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 376
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 190  df-an 378
This theorem is referenced by:  disjxiun  4392  fcof1  6203  mpt20  6380  wfrlem17  7070  eroveu  7476  boxriin  7582  undom  7678  fofinf1o  7870  finsschain  7899  suppeqfsuppbi  7915  fsuppunbi  7922  marypha1lem  7965  wemapsolem  8083  wemapso  8084  wemapso2lem  8085  cantnf  8216  iunfictbso  8563  enfin2i  8769  ttukeylem7  8963  fpwwe2lem2  9075  fpwwe2lem9  9081  fpwwe2lem12  9084  fpwwelem  9088  distrlem4pr  9469  mulcmpblnr  9513  prsrlem1  9514  dedekind  9815  divdivdiv  10330  divmuleq  10334  divadddiv  10344  divsubdiv  10345  lediv12a  10521  xmullem  11575  xlemul1a  11599  seqcaopr  12288  leexp2r  12368  hashf1lem1  12659  hashf1lem2  12660  wrd2ind  12888  cshweqrep  12977  lo1le  13792  summolem2  13859  summo  13860  prodmolem2  14066  prodmo  14067  bezoutlem3OLD  14584  bezoutlem4OLD  14585  bezoutlem3  14587  bezoutlem4  14588  qredeu  14743  pcadd  14913  prmreclem2  14940  vdwlem9  15018  vdwlem10  15019  ramub1lem2  15064  ramub1  15065  prmgaplem7  15106  cofucl  15871  setcmon  16060  poslubmo  16470  posglbmo  16471  issubmd  16674  grprcan  16777  isnsg3  16929  ghmpreima  16982  gaorber  17040  psgneu  17225  odcau  17334  lsmsubm  17383  lsmmod  17403  ablfaclem3  17798  ringpropd  17890  lmodvsmmulgdi  18204  lmodprop2d  18228  lss1d  18264  assamulgscmlem2  18650  mplcoe1  18766  mplcoe5  18769  evlslem1  18815  lindff1  19455  islindf4  19473  mdetunilem7  19720  mdetunilem8  19721  mdetunilem9  19722  mdetuni0  19723  mdetmul  19725  cayhamlem3  19988  ppttop  20099  epttop  20101  cnhaus  20447  isreg2  20470  cncmp  20484  1stcfb  20537  2ndcomap  20550  1stccnp  20554  cldllycmp  20587  1stckgenlem  20645  txcls  20696  ptcnp  20714  txdis1cn  20727  txlly  20728  txnlly  20729  pthaus  20730  txhaus  20739  txkgen  20744  xkohaus  20745  xkococnlem  20751  xkococn  20752  opnfbas  20935  hausflimi  21073  hausflim  21074  hauspwpwf1  21080  alexsubALT  21144  tgpconcomp  21205  qustgplem  21213  metequiv2  21603  met2ndci  21615  nrmmetd  21667  nlmvscnlem1  21767  reconn  21924  xrge0tsms  21930  mulc1cncf  22015  ipcnlem1  22294  minveclem3  22449  minveclem3OLD  22461  pmltpc  22479  ovolicc2lem5  22553  ovolicc2  22554  uniioombllem6  22625  dyadmbllem  22636  vitalilem3  22647  mbfmullem  22762  itg2split  22786  itg2mono  22790  dvlip2  23026  lhop1  23045  dvcnvrelem1  23048  dvfsumrlim  23062  ftc1lem6  23072  itgsubst  23080  dgrco  23308  plyexmo  23345  ulmdvlem3  23436  abelthlem2  23466  abelthlem8  23473  dvdsmulf1o  24202  chpchtsum  24226  dchrptlem2  24272  2sqlem5  24375  2sqlem9  24380  2sqb  24385  chpo1ubb  24398  vmadivsumb  24400  selbergb  24466  selberg2b  24469  selberg3lem2  24475  pntrsumbnd  24483  pntrlog2bnd  24501  pntibndlem3  24509  pnt3  24529  hlcgreu  24742  mirreu3  24778  cgraswap  24941  cgracom  24943  cgratr  24944  acopyeu  24954  axsegcon  25036  ax5seglem9  25046  axeuclid  25072  axcontlem10  25082  axcontlem12  25084  wwlknredwwlkn0  25534  clwwlkextfrlem1  25883  numclwlk1lem2f1  25901  numclwlk1lem2fo  25902  ablo4  26096  ghgrpOLD  26177  smcnlem  26414  pjhthmo  27036  pjpjpre  27153  lnconi  27767  resf1o  28390  xrge0tsmsd  28622  derangenlem  29966  pconcon  30026  conpcon  30030  cvmfolem  30074  cvmliftmolem2  30077  cvmliftmo  30079  cvmliftlem7  30086  cvmlift2lem10  30107  cvmlift3lem8  30121  linecgr  30919  btwnconn1lem8  30932  btwnconn1lem14  30938  btwnconn3  30941  brsegle  30946  segletr  30952  segleantisym  30953  outsideofeq  30968  linethru  30991  finminlem  31045  nn0prpwlem  31049  neibastop2lem  31087  mblfinlem3  32043  bddiblnc  32076  ftc1cnnc  32080  isbnd3  32180  cvlcvr1  32976  athgt  33092  4atlem12  33248  paddasslem12  33467  paddasslem13  33468  cdleme0cp  33851  cdleme42keg  34124  cdleme42mgN  34126  trlord  34207  cdlemg6c  34258  cdlemkid4  34572  dihopelvalcpre  34887  dihmeetlem1N  34929  dihglblem5apreN  34930  dihmeetlem4preN  34945  dihmeetlem6  34948  dihmeetlem10N  34955  dihmeetlem11N  34956  dihmeetlem13N  34958  dihjatcclem4  35060  mzpcl1  35642  mzpcompact2lem  35664  diophin  35686  pell14qrmulcl  35780  pwssplit4  36018  hbtlem2  36054  iunrelexpuztr  36382  stoweidlem57  38030  stoweidlem61  38034  fourierdlem92  38174  rabsubmgmd  40299  2zlidl  40442  lmodvsmdi  40675
  Copyright terms: Public domain W3C validator