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  4444  fcof1  6178  fliftfun  6198  domunfican  7793  finsschain  7827  suppeqfsuppbi  7843  fsuppunbi  7850  wemapsolem  7975  wemapso  7976  wemapso2OLD  7977  wemapso2lem  7978  cantnf  8112  cantnfOLD  8134  enfin2i  8701  ttukeylem7  8895  fpwwe2lem2  9010  fpwwe2lem9  9016  fpwwe2lem12  9019  fpwwelem  9023  distrlem4pr  9404  mulcmpblnr  9448  prsrlem1  9449  addsrmo  9450  mulsrmo  9451  divdivdiv  10245  divsubdiv  10260  lediv12a  10438  xmullem  11456  xlemul1a  11480  seqcaopr  12112  leexp2r  12191  hashf1lem1  12470  hashf1lem2  12471  brfi1uzind  12498  wrd2ind  12666  cshweqrep  12752  summolem2  13501  summo  13502  bezoutlem3  14037  bezoutlem4  14038  qredeu  14107  pcadd  14267  vdwlem9  14366  vdwlem10  14367  ramub1lem2  14404  ramub1  14405  cofucl  15115  setcmon  15272  poslubmo  15633  posglbmo  15634  grprcan  15893  isnsg3  16040  ghmpreima  16093  gaorber  16151  psgneu  16337  odcau  16430  lsmsubm  16479  lsmmod  16499  efgsfo  16563  ablfaclem3  16940  rngpropd  17031  islmodd  17318  lmodprop2d  17372  lss1d  17409  assamulgscmlem2  17797  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  evlslem1  17983  lindff1  18650  islindf4  18668  mdetunilem7  18915  mdetunilem8  18916  mdetunilem9  18917  mdetuni0  18918  mdetmul  18920  ppttop  19302  epttop  19304  cnhaus  19649  isreg2  19672  cncmp  19686  1stcfb  19740  2ndcomap  19753  cldllycmp  19790  txcls  19868  ptclsg  19879  ptcnp  19886  txdis1cn  19899  txlly  19900  txnlly  19901  pthaus  19902  txhaus  19911  txkgen  19916  xkohaus  19917  xkococnlem  19923  xkococn  19924  fgabs  20143  rnelfm  20217  hausflimi  20244  hausflim  20245  alexsubALTlem2  20311  alexsubALTlem4  20313  alexsubALT  20314  tgpconcomp  20374  divstgplem  20382  metequiv2  20776  met2ndci  20788  nrmmetd  20858  nlmvscnlem1  20958  reconn  21096  xrge0tsms  21102  ipcnlem1  21448  minveclem3  21607  pmltpc  21625  ovolicc2lem5  21695  ovolicc2  21696  uniioombllem6  21760  dyadmbllem  21771  vitalilem3  21782  mbfmullem  21895  itg2split  21919  itg2mono  21923  dvlip2  22159  lhop1  22178  dvcnvrelem1  22181  ftc1lem6  22205  itgsubst  22213  dgrco  22434  plyexmo  22471  ulmdvlem3  22559  abelthlem2  22589  abelthlem8  22596  dvdsmulf1o  23226  chpchtsum  23250  dchrptlem2  23296  2sqlem5  23399  2sqlem9  23404  2sqb  23409  pntrlog2bnd  23525  pntibndlem3  23533  pntlemp  23551  pnt3  23553  mirreu3  23776  axsegcon  23934  ax5seglem9  23944  axeuclid  23970  axcontlem12  23982  clwwlkf1  24500  wwlkext2clwwlk  24507  frgranbnb  24724  ablo4  24993  ghgrp  25074  smcnlem  25311  pjhthmo  25924  pjpjpre  26041  3oalem2  26285  lnconi  26656  atom1d  26976  resf1o  27253  xrge0tsmsd  27466  ballotlemfc0  28099  ballotlemfcc  28100  pconcon  28344  cvmfolem  28392  cvmliftmo  28397  cvmliftlem7  28404  cvmlift2lem10  28425  cvmlift3lem8  28439  prodmolem2  28672  prodmo  28673  lineext  29331  linecgr  29336  btwnconn1lem10  29351  btwnconn1lem11  29352  btwnconn3  29358  brsegle  29363  seglecgr12im  29365  segleantisym  29370  outsideoftr  29384  outsideofeq  29385  outsideofeu  29386  linethru  29408  mblfinlem3  29658  bddiblnc  29690  ftc1cnnc  29694  finminlem  29741  neibastop2lem  29809  isbnd3  29911  heibor1lem  29936  crngm4  30031  mzpcl2  30294  mzpmfp  30311  mzpmfpOLD  30312  mzpcompact2lem  30316  diophin  30338  pell14qrmulcl  30431  hbtlem2  30705  stoweidlem61  31389  fourierdlem92  31527  snlindsntor  32171  cvlcvr1  34154  4atlem12  34426  paddasslem12  34645  paddasslem13  34646  lhpexle2lem  34823  trlord  35383  cdlemkid4  35748  dihopelvalcpre  36063  dihmeetlem1N  36105  dihglblem5apreN  36106  dihmeetlem6  36124  dih1dimatlem0  36143  dihjatcclem4  36236
  Copyright terms: Public domain W3C validator