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

Theorem simprll 761
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 727 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 185  df-an 371
This theorem is referenced by:  disjxiun  4444  fcof1  6177  mpt20  6350  eroveu  7406  boxriin  7511  undom  7605  fofinf1o  7800  finsschain  7826  suppeqfsuppbi  7842  fsuppunbi  7849  marypha1lem  7892  wemapsolem  7974  wemapso  7975  wemapso2OLD  7976  wemapso2lem  7977  cantnf  8111  cantnfOLD  8133  iunfictbso  8494  enfin2i  8700  ttukeylem7  8894  fpwwe2lem2  9009  fpwwe2lem9  9015  fpwwe2lem12  9018  fpwwelem  9022  distrlem4pr  9403  mulcmpblnr  9447  prsrlem1  9448  dedekind  9742  divdivdiv  10244  divmuleq  10248  divadddiv  10258  divsubdiv  10259  lediv12a  10437  xmullem  11455  xlemul1a  11479  seqcaopr  12111  leexp2r  12190  hashf1lem1  12469  hashf1lem2  12470  wrd2ind  12665  cshweqrep  12751  lo1le  13436  summolem2  13500  summo  13501  bezoutlem3  14036  bezoutlem4  14037  qredeu  14106  pcadd  14266  prmreclem2  14293  vdwlem9  14365  vdwlem10  14366  ramub1lem2  14403  ramub1  14404  cofucl  15114  setcmon  15271  poslubmo  15632  posglbmo  15633  issubmd  15796  grprcan  15890  isnsg3  16037  ghmpreima  16090  gaorber  16148  psgneu  16334  odcau  16427  lsmsubm  16476  lsmmod  16496  ablfaclem3  16937  rngpropd  17026  lmodvsmmulgdi  17342  lmodprop2d  17367  lss1d  17404  assamulgscmlem2  17785  mplcoe1  17914  mplcoe5  17918  mplcoe2OLD  17920  evlslem1  17971  lindff1  18638  islindf4  18656  mdetunilem7  18903  mdetunilem8  18904  mdetunilem9  18905  mdetuni0  18906  mdetmul  18908  cayhamlem3  19171  ppttop  19290  epttop  19292  cnhaus  19637  isreg2  19660  cncmp  19674  1stcfb  19728  2ndcomap  19741  1stccnp  19745  cldllycmp  19778  1stckgenlem  19805  txcls  19856  ptcnp  19874  txdis1cn  19887  txlly  19888  txnlly  19889  pthaus  19890  txhaus  19899  txkgen  19904  xkohaus  19905  xkococnlem  19911  xkococn  19912  opnfbas  20094  hausflimi  20232  hausflim  20233  hauspwpwf1  20239  alexsubALT  20302  tgpconcomp  20362  divstgplem  20370  metequiv2  20764  met2ndci  20776  nrmmetd  20846  nlmvscnlem1  20946  reconn  21084  xrge0tsms  21090  mulc1cncf  21160  ipcnlem1  21436  minveclem3  21595  pmltpc  21613  ovolicc2lem5  21683  ovolicc2  21684  uniioombllem6  21748  dyadmbllem  21759  vitalilem3  21770  mbfmullem  21883  itg2split  21907  itg2mono  21911  dvlip2  22147  lhop1  22166  dvcnvrelem1  22169  dvfsumrlim  22183  ftc1lem6  22193  itgsubst  22201  dgrco  22422  plyexmo  22459  ulmdvlem3  22547  abelthlem2  22577  abelthlem8  22584  dvdsmulf1o  23214  chpchtsum  23238  dchrptlem2  23284  2sqlem5  23387  2sqlem9  23392  2sqb  23397  chpo1ubb  23410  vmadivsumb  23412  selbergb  23478  selberg2b  23481  selberg3lem2  23487  pntrsumbnd  23495  pntrlog2bnd  23513  pntibndlem3  23521  pnt3  23541  mirreu3  23764  axsegcon  23922  ax5seglem9  23932  axeuclid  23958  axcontlem10  23968  axcontlem12  23970  wwlknredwwlkn0  24419  clwwlkextfrlem1  24769  numclwlk1lem2f1  24787  numclwlk1lem2fo  24788  ablo4  24981  ghgrp  25062  smcnlem  25299  pjhthmo  25912  pjpjpre  26029  lnconi  26644  resf1o  27241  xrge0tsmsd  27454  derangenlem  28271  pconcon  28332  conpcon  28336  cvmfolem  28380  cvmliftmolem2  28383  cvmliftmo  28385  cvmliftlem7  28392  cvmlift2lem10  28413  cvmlift3lem8  28427  prodmolem2  28660  prodmo  28661  linecgr  29324  btwnconn1lem8  29337  btwnconn1lem14  29343  btwnconn3  29346  brsegle  29351  segletr  29357  segleantisym  29358  outsideofeq  29373  linethru  29396  mblfinlem3  29646  bddiblnc  29678  ftc1cnnc  29682  finminlem  29729  nn0prpwlem  29733  neibastop2lem  29797  isbnd3  29899  mzpcl1  30281  mzpcompact2lem  30304  diophin  30326  pell14qrmulcl  30419  pwssplit4  30655  hbtlem2  30693  stoweidlem57  31373  stoweidlem61  31377  fourierdlem92  31515  lmodvsmdi  32065  cvlcvr1  34145  athgt  34261  4atlem12  34417  paddasslem12  34636  paddasslem13  34637  cdleme0cp  35019  cdleme42keg  35291  cdleme42mgN  35293  trlord  35374  cdlemg6c  35425  cdlemkid4  35739  dihopelvalcpre  36054  dihmeetlem1N  36096  dihglblem5apreN  36097  dihmeetlem4preN  36112  dihmeetlem6  36115  dihmeetlem10N  36122  dihmeetlem11N  36123  dihmeetlem13N  36125  dihjatcclem4  36227
  Copyright terms: Public domain W3C validator