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  4036  fcof1  5813  fliftfun  5827  domunfican  7145  finsschain  7178  wemapso2lem  7281  wemapso  7282  wemapso2  7283  cantnf  7411  enfin2i  7963  ttukeylem7  8158  fpwwe2lem2  8270  fpwwe2lem9  8276  fpwwe2lem12  8279  fpwwelem  8283  distrlem4pr  8666  divdivdiv  9477  divsubdiv  9492  lediv12a  9665  xmullem  10600  xlemul1a  10624  seqcaopr  11099  leexp2r  11175  hashf1lem1  11409  hashf1lem2  11410  summolem2  12205  summo  12206  bezoutlem3  12735  bezoutlem4  12736  qredeu  12802  pcadd  12953  vdwlem9  13052  vdwlem10  13053  ramub1lem2  13090  ramub1  13091  cofucl  13778  setcmon  13935  poslubmo  14266  grprcan  14531  isnsg3  14667  ghmpreima  14720  gaorber  14778  odcau  14931  lsmsubm  14980  lsmmod  15000  efgsfo  15064  ablfaclem3  15338  rngpropd  15388  islmodd  15649  lmodprop2d  15703  lss1d  15736  mplcoe1  16225  mplcoe2  16227  ppttop  16760  epttop  16762  cnhaus  17098  isreg2  17121  cncmp  17135  1stcfb  17187  2ndcomap  17200  cldllycmp  17237  txcls  17315  ptclsg  17325  ptcnp  17332  txdis1cn  17345  txlly  17346  txnlly  17347  pthaus  17348  txhaus  17357  txkgen  17362  xkohaus  17363  xkococnlem  17369  xkococn  17370  fgabs  17590  rnelfm  17664  hausflimi  17691  hausflim  17692  alexsubALTlem2  17758  alexsubALTlem4  17760  alexsubALT  17761  tgpconcomp  17811  divstgplem  17819  metequiv2  18072  met2ndci  18084  nrmmetd  18113  nlmvscnlem1  18213  reconn  18349  xrge0tsms  18355  ipcnlem1  18688  minveclem3  18809  pmltpc  18826  ovolicc2lem5  18896  ovolicc2  18897  uniioombllem6  18959  dyadmbllem  18970  vitalilem3  18981  mbfmullem  19096  itg2split  19120  itg2mono  19124  dvlip2  19358  lhop1  19377  dvcnvrelem1  19380  ftc1lem6  19404  itgsubst  19412  evlslem1  19415  dgrco  19672  plyexmo  19709  ulmdvlem3  19795  abelthlem2  19824  abelthlem8  19831  dvdsmulf1o  20450  chpchtsum  20474  dchrptlem2  20520  2sqlem5  20623  2sqlem9  20628  2sqb  20633  pntrlog2bnd  20749  pntibndlem3  20757  pntlemp  20775  pnt3  20777  ablo4  20970  ghgrp  21051  smcnlem  21286  pjhthmo  21897  pjpjpre  22014  3oalem2  22258  lnconi  22629  atom1d  22949  ballotlemfc0  23067  ballotlemfcc  23068  xrge0tsmsd  23397  pconcon  23777  cvmfolem  23825  cvmliftmo  23830  cvmliftlem7  23837  cvmlift2lem10  23858  cvmlift3lem8  23872  prodmolem2  24158  prodmo  24159  axsegcon  24627  ax5seglem9  24637  axeuclid  24663  axcontlem12  24675  lineext  24771  linecgr  24776  btwnconn1lem10  24791  btwnconn1lem11  24792  btwnconn3  24798  brsegle  24803  seglecgr12im  24805  segleantisym  24810  outsideoftr  24824  outsideofeq  24825  outsideofeu  24826  linethru  24848  itg2addnc  25005  bddiblnc  25021  ftc1cnnc  25025  injsurinj  25252  resgcom  25454  fprodsub  25482  icccon3  25804  pdiveql  26271  finminlem  26334  neibastop2lem  26412  isbnd3  26611  heibor1lem  26636  crngm4  26731  mzpcl2  26911  mzpmfp  26928  mzpcompact2lem  26932  diophin  26955  pell14qrmulcl  27051  lindff1  27393  islindf4  27411  hbtlem2  27431  psgneu  27532  cvlcvr1  30151  4atlem12  30423  paddasslem12  30642  paddasslem13  30643  lhpexle2lem  30820  trlord  31380  cdlemkid4  31745  dihopelvalcpre  32060  dihmeetlem1N  32102  dihglblem5apreN  32103  dihmeetlem6  32121  dih1dimatlem0  32140  dihjatcclem4  32233
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