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

Theorem simprlr 771
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 462 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 732 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  disjxiun  4417  fcof1  6197  fliftfun  6217  wfrlem17  7057  domunfican  7847  finsschain  7884  suppeqfsuppbi  7900  fsuppunbi  7907  wemapsolem  8068  wemapso  8069  wemapso2lem  8070  cantnf  8200  enfin2i  8752  ttukeylem7  8946  fpwwe2lem2  9058  fpwwe2lem9  9064  fpwwe2lem12  9067  fpwwelem  9071  distrlem4pr  9452  mulcmpblnr  9496  prsrlem1  9497  addsrmo  9498  mulsrmo  9499  divdivdiv  10309  divsubdiv  10324  lediv12a  10500  xmullem  11551  xlemul1a  11575  seqcaopr  12250  leexp2r  12330  hashf1lem1  12616  hashf1lem2  12617  brfi1uzind  12647  wrd2ind  12825  cshweqrep  12911  summolem2  13770  summo  13771  prodmolem2  13977  prodmo  13978  bezoutlem3OLD  14493  bezoutlem4OLD  14494  bezoutlem3  14496  bezoutlem4  14497  qredeu  14652  pcadd  14822  vdwlem9  14927  vdwlem10  14928  ramub1lem2  14973  ramub1  14974  cofucl  15781  setcmon  15970  poslubmo  16380  posglbmo  16381  grprcan  16687  isnsg3  16839  ghmpreima  16892  gaorber  16950  psgneu  17135  odcau  17244  lsmsubm  17293  lsmmod  17313  efgsfo  17377  ablfaclem3  17708  ringpropd  17800  islmodd  18085  lmodprop2d  18138  lss1d  18174  assamulgscmlem2  18561  mplcoe1  18677  mplcoe5  18680  evlslem1  18726  lindff1  19365  islindf4  19383  mdetunilem7  19630  mdetunilem8  19631  mdetunilem9  19632  mdetuni0  19633  mdetmul  19635  ppttop  20009  epttop  20011  cnhaus  20357  isreg2  20380  cncmp  20394  1stcfb  20447  2ndcomap  20460  cldllycmp  20497  txcls  20606  ptclsg  20617  ptcnp  20624  txdis1cn  20637  txlly  20638  txnlly  20639  pthaus  20640  txhaus  20649  txkgen  20654  xkohaus  20655  xkococnlem  20661  xkococn  20662  fgabs  20881  rnelfm  20955  hausflimi  20982  hausflim  20983  alexsubALTlem2  21050  alexsubALTlem4  21052  alexsubALT  21053  tgpconcomp  21114  qustgplem  21122  metequiv2  21512  met2ndci  21524  nrmmetd  21576  nlmvscnlem1  21676  reconn  21833  xrge0tsms  21839  ipcnlem1  22203  minveclem3  22358  minveclem3OLD  22370  pmltpc  22388  ovolicc2lem5  22462  ovolicc2  22463  uniioombllem6  22533  dyadmbllem  22544  vitalilem3  22555  mbfmullem  22670  itg2split  22694  itg2mono  22698  dvlip2  22934  lhop1  22953  dvcnvrelem1  22956  ftc1lem6  22980  itgsubst  22988  dgrco  23216  plyexmo  23253  ulmdvlem3  23344  abelthlem2  23374  abelthlem8  23381  dvdsmulf1o  24110  chpchtsum  24134  dchrptlem2  24180  2sqlem5  24283  2sqlem9  24288  2sqb  24293  pntrlog2bnd  24409  pntibndlem3  24417  pntlemp  24435  pnt3  24437  hlcgreu  24650  mirreu3  24686  cgraswap  24849  cgracom  24851  cgratr  24852  acopyeu  24862  axsegcon  24944  ax5seglem9  24954  axeuclid  24980  axcontlem12  24992  clwwlkf1  25510  wwlkext2clwwlk  25517  frgranbnb  25734  ablo4  26001  ghgrpOLD  26082  smcnlem  26319  pjhthmo  26941  pjpjpre  27058  3oalem2  27302  lnconi  27672  atom1d  27992  resf1o  28309  xrge0tsmsd  28544  ballotlemfc0  29321  ballotlemfcc  29322  pconcon  29950  cvmfolem  29998  cvmliftmo  30003  cvmliftlem7  30010  cvmlift2lem10  30031  cvmlift3lem8  30045  lineext  30836  linecgr  30841  btwnconn1lem10  30856  btwnconn1lem11  30857  btwnconn3  30863  brsegle  30868  seglecgr12im  30870  segleantisym  30875  outsideoftr  30889  outsideofeq  30890  outsideofeu  30891  linethru  30913  finminlem  30967  neibastop2lem  31009  isbasisrelowllem1  31699  isbasisrelowllem2  31700  mblfinlem3  31893  bddiblnc  31926  ftc1cnnc  31930  isbnd3  32030  heibor1lem  32055  crngm4  32150  cvlcvr1  32824  4atlem12  33096  paddasslem12  33315  paddasslem13  33316  lhpexle2lem  33493  trlord  34055  cdlemkid4  34420  dihopelvalcpre  34735  dihmeetlem1N  34777  dihglblem5apreN  34778  dihmeetlem6  34796  dih1dimatlem0  34815  dihjatcclem4  34908  mzpcl2  35491  mzpmfp  35508  mzpcompact2lem  35512  diophin  35534  pell14qrmulcl  35629  hbtlem2  35903  iunrelexpuztr  36171  stoweidlem61  37742  fourierdlem92  37882  snlindsntor  39538  elfzolborelfzop1  39590  nn0sumshdiglemB  39705
  Copyright terms: Public domain W3C validator