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

Theorem simprlr 755
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 458 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 720 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  4277  fcof1  5978  fliftfun  5992  domunfican  7572  finsschain  7606  suppeqfsuppbi  7622  fsuppunbi  7629  wemapsolem  7752  wemapso  7753  wemapso2OLD  7754  wemapso2lem  7755  cantnf  7889  cantnfOLD  7911  enfin2i  8478  ttukeylem7  8672  fpwwe2lem2  8786  fpwwe2lem9  8792  fpwwe2lem12  8795  fpwwelem  8799  distrlem4pr  9182  divdivdiv  10019  divsubdiv  10034  lediv12a  10212  xmullem  11214  xlemul1a  11238  seqcaopr  11826  leexp2r  11904  hashf1lem1  12191  hashf1lem2  12192  brfi1uzind  12202  wrd2ind  12355  cshweqrep  12438  summolem2  13176  summo  13177  bezoutlem3  13706  bezoutlem4  13707  qredeu  13775  pcadd  13933  vdwlem9  14032  vdwlem10  14033  ramub1lem2  14070  ramub1  14071  cofucl  14780  setcmon  14937  poslubmo  15298  posglbmo  15299  grprcan  15550  isnsg3  15694  ghmpreima  15747  gaorber  15805  psgneu  15991  odcau  16082  lsmsubm  16131  lsmmod  16151  efgsfo  16215  ablfaclem3  16561  rngpropd  16611  islmodd  16877  lmodprop2d  16930  lss1d  16965  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  lindff1  18090  islindf4  18108  mdetunilem7  18265  mdetunilem8  18266  mdetunilem9  18267  mdetuni0  18268  mdetmul  18270  ppttop  18452  epttop  18454  cnhaus  18799  isreg2  18822  cncmp  18836  1stcfb  18890  2ndcomap  18903  cldllycmp  18940  txcls  19018  ptclsg  19029  ptcnp  19036  txdis1cn  19049  txlly  19050  txnlly  19051  pthaus  19052  txhaus  19061  txkgen  19066  xkohaus  19067  xkococnlem  19073  xkococn  19074  fgabs  19293  rnelfm  19367  hausflimi  19394  hausflim  19395  alexsubALTlem2  19461  alexsubALTlem4  19463  alexsubALT  19464  tgpconcomp  19524  divstgplem  19532  metequiv2  19926  met2ndci  19938  nrmmetd  20008  nlmvscnlem1  20108  reconn  20246  xrge0tsms  20252  ipcnlem1  20598  minveclem3  20757  pmltpc  20775  ovolicc2lem5  20845  ovolicc2  20846  uniioombllem6  20909  dyadmbllem  20920  vitalilem3  20931  mbfmullem  21044  itg2split  21068  itg2mono  21072  dvlip2  21308  lhop1  21327  dvcnvrelem1  21330  ftc1lem6  21354  itgsubst  21362  evlslem1  21366  dgrco  21626  plyexmo  21663  ulmdvlem3  21751  abelthlem2  21781  abelthlem8  21788  dvdsmulf1o  22418  chpchtsum  22442  dchrptlem2  22488  2sqlem5  22591  2sqlem9  22596  2sqb  22601  pntrlog2bnd  22717  pntibndlem3  22725  pntlemp  22743  pnt3  22745  mirreu3  22923  axsegcon  22995  ax5seglem9  23005  axeuclid  23031  axcontlem12  23043  ablo4  23596  ghgrp  23677  smcnlem  23914  pjhthmo  24527  pjpjpre  24644  3oalem2  24888  lnconi  25259  atom1d  25579  resf1o  25854  xrge0tsmsd  26105  ballotlemfc0  26722  ballotlemfcc  26723  pconcon  26967  cvmfolem  27015  cvmliftmo  27020  cvmliftlem7  27027  cvmlift2lem10  27048  cvmlift3lem8  27062  prodmolem2  27294  prodmo  27295  lineext  27953  linecgr  27958  btwnconn1lem10  27973  btwnconn1lem11  27974  btwnconn3  27980  brsegle  27985  seglecgr12im  27987  segleantisym  27992  outsideoftr  28006  outsideofeq  28007  outsideofeu  28008  linethru  28030  mblfinlem3  28271  bddiblnc  28303  ftc1cnnc  28307  finminlem  28354  neibastop2lem  28422  isbnd3  28524  heibor1lem  28549  crngm4  28644  mzpcl2  28908  mzpmfp  28925  mzpmfpOLD  28926  mzpcompact2lem  28930  diophin  28953  pell14qrmulcl  29046  hbtlem2  29322  stoweidlem61  29699  clwwlkf1  30301  wwlkext2clwwlk  30308  frgranbnb  30455  snlindsntor  30711  cvlcvr1  32554  4atlem12  32826  paddasslem12  33045  paddasslem13  33046  lhpexle2lem  33223  trlord  33783  cdlemkid4  34148  dihopelvalcpre  34463  dihmeetlem1N  34505  dihglblem5apreN  34506  dihmeetlem6  34524  dih1dimatlem0  34543  dihjatcclem4  34636
  Copyright terms: Public domain W3C validator