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

Theorem simprlr 739
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 447 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 708 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  disjxiun  4020  fcof1  5797  fliftfun  5811  domunfican  7129  finsschain  7162  wemapso2lem  7265  wemapso  7266  wemapso2  7267  cantnf  7395  enfin2i  7947  ttukeylem7  8142  fpwwe2lem2  8254  fpwwe2lem9  8260  fpwwe2lem12  8263  fpwwelem  8267  distrlem4pr  8650  divdivdiv  9461  divsubdiv  9476  lediv12a  9649  xmullem  10584  xlemul1a  10608  seqcaopr  11083  leexp2r  11159  hashf1lem1  11393  hashf1lem2  11394  summolem2  12189  summo  12190  bezoutlem3  12719  bezoutlem4  12720  qredeu  12786  pcadd  12937  vdwlem9  13036  vdwlem10  13037  ramub1lem2  13074  ramub1  13075  cofucl  13762  setcmon  13919  poslubmo  14250  grprcan  14515  isnsg3  14651  ghmpreima  14704  gaorber  14762  odcau  14915  lsmsubm  14964  lsmmod  14984  efgsfo  15048  ablfaclem3  15322  rngpropd  15372  islmodd  15633  lmodprop2d  15687  lss1d  15720  mplcoe1  16209  mplcoe2  16211  ppttop  16744  epttop  16746  cnhaus  17082  isreg2  17105  cncmp  17119  1stcfb  17171  2ndcomap  17184  cldllycmp  17221  txcls  17299  ptclsg  17309  ptcnp  17316  txdis1cn  17329  txlly  17330  txnlly  17331  pthaus  17332  txhaus  17341  txkgen  17346  xkohaus  17347  xkococnlem  17353  xkococn  17354  fgabs  17574  rnelfm  17648  hausflimi  17675  hausflim  17676  alexsubALTlem2  17742  alexsubALTlem4  17744  alexsubALT  17745  tgpconcomp  17795  divstgplem  17803  metequiv2  18056  met2ndci  18068  nrmmetd  18097  nlmvscnlem1  18197  reconn  18333  xrge0tsms  18339  ipcnlem1  18672  minveclem3  18793  pmltpc  18810  ovolicc2lem5  18880  ovolicc2  18881  uniioombllem6  18943  dyadmbllem  18954  vitalilem3  18965  mbfmullem  19080  itg2split  19104  itg2mono  19108  dvlip2  19342  lhop1  19361  dvcnvrelem1  19364  ftc1lem6  19388  itgsubst  19396  evlslem1  19399  dgrco  19656  plyexmo  19693  ulmdvlem3  19779  abelthlem2  19808  abelthlem8  19815  dvdsmulf1o  20434  chpchtsum  20458  dchrptlem2  20504  2sqlem5  20607  2sqlem9  20612  2sqb  20617  pntrlog2bnd  20733  pntibndlem3  20741  pntlemp  20759  pnt3  20761  ablo4  20954  ghgrp  21035  smcnlem  21270  pjhthmo  21881  pjpjpre  21998  3oalem2  22242  lnconi  22613  atom1d  22933  ballotlemfc0  23051  ballotlemfcc  23052  xrge0tsmsd  23382  pconcon  23762  cvmfolem  23810  cvmliftmo  23815  cvmliftlem7  23822  cvmlift2lem10  23843  cvmlift3lem8  23857  axsegcon  24555  ax5seglem9  24565  axeuclid  24591  axcontlem12  24603  lineext  24699  linecgr  24704  btwnconn1lem10  24719  btwnconn1lem11  24720  btwnconn3  24726  brsegle  24731  seglecgr12im  24733  segleantisym  24738  outsideoftr  24752  outsideofeq  24753  outsideofeu  24754  linethru  24776  injsurinj  25149  resgcom  25351  fprodsub  25379  icccon3  25701  pdiveql  26168  finminlem  26231  neibastop2lem  26309  isbnd3  26508  heibor1lem  26533  crngm4  26628  mzpcl2  26808  mzpmfp  26825  mzpcompact2lem  26829  diophin  26852  pell14qrmulcl  26948  lindff1  27290  islindf4  27308  hbtlem2  27328  psgneu  27429  cvlcvr1  29529  4atlem12  29801  paddasslem12  30020  paddasslem13  30021  lhpexle2lem  30198  trlord  30758  cdlemkid4  31123  dihopelvalcpre  31438  dihmeetlem1N  31480  dihglblem5apreN  31481  dihmeetlem6  31499  dih1dimatlem0  31518  dihjatcclem4  31611
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 177  df-an 360
  Copyright terms: Public domain W3C validator