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

Theorem simprlr 740
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 448 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 709 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  disjxiun  4201  fcof1  6011  fliftfun  6025  domunfican  7370  finsschain  7404  wemapso2lem  7508  wemapso  7509  wemapso2  7510  cantnf  7638  enfin2i  8190  ttukeylem7  8384  fpwwe2lem2  8496  fpwwe2lem9  8502  fpwwe2lem12  8505  fpwwelem  8509  distrlem4pr  8892  divdivdiv  9704  divsubdiv  9719  lediv12a  9892  xmullem  10832  xlemul1a  10856  seqcaopr  11348  leexp2r  11425  hashf1lem1  11692  hashf1lem2  11693  brfi1uzind  11703  summolem2  12498  summo  12499  bezoutlem3  13028  bezoutlem4  13029  qredeu  13095  pcadd  13246  vdwlem9  13345  vdwlem10  13346  ramub1lem2  13383  ramub1  13384  cofucl  14073  setcmon  14230  poslubmo  14561  grprcan  14826  isnsg3  14962  ghmpreima  15015  gaorber  15073  odcau  15226  lsmsubm  15275  lsmmod  15295  efgsfo  15359  ablfaclem3  15633  rngpropd  15683  islmodd  15944  lmodprop2d  15994  lss1d  16027  mplcoe1  16516  mplcoe2  16518  ppttop  17059  epttop  17061  cnhaus  17406  isreg2  17429  cncmp  17443  1stcfb  17496  2ndcomap  17509  cldllycmp  17546  txcls  17624  ptclsg  17635  ptcnp  17642  txdis1cn  17655  txlly  17656  txnlly  17657  pthaus  17658  txhaus  17667  txkgen  17672  xkohaus  17673  xkococnlem  17679  xkococn  17680  fgabs  17899  rnelfm  17973  hausflimi  18000  hausflim  18001  alexsubALTlem2  18067  alexsubALTlem4  18069  alexsubALT  18070  tgpconcomp  18130  divstgplem  18138  metequiv2  18528  met2ndci  18540  nrmmetd  18610  nlmvscnlem1  18710  reconn  18847  xrge0tsms  18853  ipcnlem1  19187  minveclem3  19318  pmltpc  19335  ovolicc2lem5  19405  ovolicc2  19406  uniioombllem6  19468  dyadmbllem  19479  vitalilem3  19490  mbfmullem  19605  itg2split  19629  itg2mono  19633  dvlip2  19867  lhop1  19886  dvcnvrelem1  19889  ftc1lem6  19913  itgsubst  19921  evlslem1  19924  dgrco  20181  plyexmo  20218  ulmdvlem3  20306  abelthlem2  20336  abelthlem8  20343  dvdsmulf1o  20967  chpchtsum  20991  dchrptlem2  21037  2sqlem5  21140  2sqlem9  21145  2sqb  21150  pntrlog2bnd  21266  pntibndlem3  21274  pntlemp  21292  pnt3  21294  ablo4  21863  ghgrp  21944  smcnlem  22181  pjhthmo  22792  pjpjpre  22909  3oalem2  23153  lnconi  23524  atom1d  23844  xrge0tsmsd  24211  ballotlemfc0  24738  ballotlemfcc  24739  pconcon  24906  cvmfolem  24954  cvmliftmo  24959  cvmliftlem7  24966  cvmlift2lem10  24987  cvmlift3lem8  25001  prodmolem2  25250  prodmo  25251  axsegcon  25814  ax5seglem9  25824  axeuclid  25850  axcontlem12  25862  lineext  25958  linecgr  25963  btwnconn1lem10  25978  btwnconn1lem11  25979  btwnconn3  25985  brsegle  25990  seglecgr12im  25992  segleantisym  25997  outsideoftr  26011  outsideofeq  26012  outsideofeu  26013  linethru  26035  mblfinlem2  26191  bddiblnc  26221  ftc1cnnc  26225  finminlem  26258  neibastop2lem  26326  isbnd3  26430  heibor1lem  26455  crngm4  26550  mzpcl2  26724  mzpmfp  26741  mzpcompact2lem  26745  diophin  26768  pell14qrmulcl  26863  lindff1  27205  islindf4  27223  hbtlem2  27243  psgneu  27344  stoweidlem61  27724  shwrdsdisj  28173  frgranbnb  28268  cvlcvr1  29976  4atlem12  30248  paddasslem12  30467  paddasslem13  30468  lhpexle2lem  30645  trlord  31205  cdlemkid4  31570  dihopelvalcpre  31885  dihmeetlem1N  31927  dihglblem5apreN  31928  dihmeetlem6  31946  dih1dimatlem0  31965  dihjatcclem4  32058
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361
  Copyright terms: Public domain W3C validator