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

Theorem simprlr 762
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprlr  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 461 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 727 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
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  4310  fcof1  6012  fliftfun  6026  domunfican  7605  finsschain  7639  suppeqfsuppbi  7655  fsuppunbi  7662  wemapsolem  7785  wemapso  7786  wemapso2OLD  7787  wemapso2lem  7788  cantnf  7922  cantnfOLD  7944  enfin2i  8511  ttukeylem7  8705  fpwwe2lem2  8820  fpwwe2lem9  8826  fpwwe2lem12  8829  fpwwelem  8833  distrlem4pr  9216  divdivdiv  10053  divsubdiv  10068  lediv12a  10246  xmullem  11248  xlemul1a  11272  seqcaopr  11864  leexp2r  11942  hashf1lem1  12229  hashf1lem2  12230  brfi1uzind  12240  wrd2ind  12393  cshweqrep  12476  summolem2  13214  summo  13215  bezoutlem3  13745  bezoutlem4  13746  qredeu  13814  pcadd  13972  vdwlem9  14071  vdwlem10  14072  ramub1lem2  14109  ramub1  14110  cofucl  14819  setcmon  14976  poslubmo  15337  posglbmo  15338  grprcan  15592  isnsg3  15736  ghmpreima  15789  gaorber  15847  psgneu  16033  odcau  16124  lsmsubm  16173  lsmmod  16193  efgsfo  16257  ablfaclem3  16610  rngpropd  16698  islmodd  16976  lmodprop2d  17029  lss1d  17066  mplcoe1  17566  mplcoe5  17570  mplcoe2OLD  17572  evlslem1  17623  lindff1  18271  islindf4  18289  mdetunilem7  18446  mdetunilem8  18447  mdetunilem9  18448  mdetuni0  18449  mdetmul  18451  ppttop  18633  epttop  18635  cnhaus  18980  isreg2  19003  cncmp  19017  1stcfb  19071  2ndcomap  19084  cldllycmp  19121  txcls  19199  ptclsg  19210  ptcnp  19217  txdis1cn  19230  txlly  19231  txnlly  19232  pthaus  19233  txhaus  19242  txkgen  19247  xkohaus  19248  xkococnlem  19254  xkococn  19255  fgabs  19474  rnelfm  19548  hausflimi  19575  hausflim  19576  alexsubALTlem2  19642  alexsubALTlem4  19644  alexsubALT  19645  tgpconcomp  19705  divstgplem  19713  metequiv2  20107  met2ndci  20119  nrmmetd  20189  nlmvscnlem1  20289  reconn  20427  xrge0tsms  20433  ipcnlem1  20779  minveclem3  20938  pmltpc  20956  ovolicc2lem5  21026  ovolicc2  21027  uniioombllem6  21090  dyadmbllem  21101  vitalilem3  21112  mbfmullem  21225  itg2split  21249  itg2mono  21253  dvlip2  21489  lhop1  21508  dvcnvrelem1  21511  ftc1lem6  21535  itgsubst  21543  dgrco  21764  plyexmo  21801  ulmdvlem3  21889  abelthlem2  21919  abelthlem8  21926  dvdsmulf1o  22556  chpchtsum  22580  dchrptlem2  22626  2sqlem5  22729  2sqlem9  22734  2sqb  22739  pntrlog2bnd  22855  pntibndlem3  22863  pntlemp  22881  pnt3  22883  mirreu3  23080  axsegcon  23195  ax5seglem9  23205  axeuclid  23231  axcontlem12  23243  ablo4  23796  ghgrp  23877  smcnlem  24114  pjhthmo  24727  pjpjpre  24844  3oalem2  25088  lnconi  25459  atom1d  25779  resf1o  26052  xrge0tsmsd  26275  ballotlemfc0  26897  ballotlemfcc  26898  pconcon  27142  cvmfolem  27190  cvmliftmo  27195  cvmliftlem7  27202  cvmlift2lem10  27223  cvmlift3lem8  27237  prodmolem2  27470  prodmo  27471  lineext  28129  linecgr  28134  btwnconn1lem10  28149  btwnconn1lem11  28150  btwnconn3  28156  brsegle  28161  seglecgr12im  28163  segleantisym  28168  outsideoftr  28182  outsideofeq  28183  outsideofeu  28184  linethru  28206  mblfinlem3  28456  bddiblnc  28488  ftc1cnnc  28492  finminlem  28539  neibastop2lem  28607  isbnd3  28709  heibor1lem  28734  crngm4  28829  mzpcl2  29092  mzpmfp  29109  mzpmfpOLD  29110  mzpcompact2lem  29114  diophin  29137  pell14qrmulcl  29230  hbtlem2  29506  stoweidlem61  29882  clwwlkf1  30484  wwlkext2clwwlk  30491  frgranbnb  30638  assamulgscmlem2  30854  scmatmulcl  30925  snlindsntor  31002  cvlcvr1  33080  4atlem12  33352  paddasslem12  33571  paddasslem13  33572  lhpexle2lem  33749  trlord  34309  cdlemkid4  34674  dihopelvalcpre  34989  dihmeetlem1N  35031  dihglblem5apreN  35032  dihmeetlem6  35050  dih1dimatlem0  35069  dihjatcclem4  35162
  Copyright terms: Public domain W3C validator