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

Theorem simprlr 740
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 448 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 709 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  disjxiun  4169  fcof1  5979  fliftfun  5993  domunfican  7338  finsschain  7371  wemapso2lem  7475  wemapso  7476  wemapso2  7477  cantnf  7605  enfin2i  8157  ttukeylem7  8351  fpwwe2lem2  8463  fpwwe2lem9  8469  fpwwe2lem12  8472  fpwwelem  8476  distrlem4pr  8859  divdivdiv  9671  divsubdiv  9686  lediv12a  9859  xmullem  10799  xlemul1a  10823  seqcaopr  11315  leexp2r  11392  hashf1lem1  11659  hashf1lem2  11660  brfi1uzind  11670  summolem2  12465  summo  12466  bezoutlem3  12995  bezoutlem4  12996  qredeu  13062  pcadd  13213  vdwlem9  13312  vdwlem10  13313  ramub1lem2  13350  ramub1  13351  cofucl  14040  setcmon  14197  poslubmo  14528  grprcan  14793  isnsg3  14929  ghmpreima  14982  gaorber  15040  odcau  15193  lsmsubm  15242  lsmmod  15262  efgsfo  15326  ablfaclem3  15600  rngpropd  15650  islmodd  15911  lmodprop2d  15961  lss1d  15994  mplcoe1  16483  mplcoe2  16485  ppttop  17026  epttop  17028  cnhaus  17372  isreg2  17395  cncmp  17409  1stcfb  17461  2ndcomap  17474  cldllycmp  17511  txcls  17589  ptclsg  17600  ptcnp  17607  txdis1cn  17620  txlly  17621  txnlly  17622  pthaus  17623  txhaus  17632  txkgen  17637  xkohaus  17638  xkococnlem  17644  xkococn  17645  fgabs  17864  rnelfm  17938  hausflimi  17965  hausflim  17966  alexsubALTlem2  18032  alexsubALTlem4  18034  alexsubALT  18035  tgpconcomp  18095  divstgplem  18103  metequiv2  18493  met2ndci  18505  nrmmetd  18575  nlmvscnlem1  18675  reconn  18812  xrge0tsms  18818  ipcnlem1  19152  minveclem3  19283  pmltpc  19300  ovolicc2lem5  19370  ovolicc2  19371  uniioombllem6  19433  dyadmbllem  19444  vitalilem3  19455  mbfmullem  19570  itg2split  19594  itg2mono  19598  dvlip2  19832  lhop1  19851  dvcnvrelem1  19854  ftc1lem6  19878  itgsubst  19886  evlslem1  19889  dgrco  20146  plyexmo  20183  ulmdvlem3  20271  abelthlem2  20301  abelthlem8  20308  dvdsmulf1o  20932  chpchtsum  20956  dchrptlem2  21002  2sqlem5  21105  2sqlem9  21110  2sqb  21115  pntrlog2bnd  21231  pntibndlem3  21239  pntlemp  21257  pnt3  21259  ablo4  21828  ghgrp  21909  smcnlem  22146  pjhthmo  22757  pjpjpre  22874  3oalem2  23118  lnconi  23489  atom1d  23809  xrge0tsmsd  24176  ballotlemfc0  24703  ballotlemfcc  24704  pconcon  24871  cvmfolem  24919  cvmliftmo  24924  cvmliftlem7  24931  cvmlift2lem10  24952  cvmlift3lem8  24966  prodmolem2  25214  prodmo  25215  axsegcon  25770  ax5seglem9  25780  axeuclid  25806  axcontlem12  25818  lineext  25914  linecgr  25919  btwnconn1lem10  25934  btwnconn1lem11  25935  btwnconn3  25941  brsegle  25946  seglecgr12im  25948  segleantisym  25953  outsideoftr  25967  outsideofeq  25968  outsideofeu  25969  linethru  25991  mblfinlem2  26144  bddiblnc  26174  ftc1cnnc  26178  finminlem  26211  neibastop2lem  26279  isbnd3  26383  heibor1lem  26408  crngm4  26503  mzpcl2  26677  mzpmfp  26694  mzpcompact2lem  26698  diophin  26721  pell14qrmulcl  26816  lindff1  27158  islindf4  27176  hbtlem2  27196  psgneu  27297  stoweidlem61  27677  frgranbnb  28124  cvlcvr1  29822  4atlem12  30094  paddasslem12  30313  paddasslem13  30314  lhpexle2lem  30491  trlord  31051  cdlemkid4  31416  dihopelvalcpre  31731  dihmeetlem1N  31773  dihglblem5apreN  31774  dihmeetlem6  31792  dih1dimatlem0  31811  dihjatcclem4  31904
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 178  df-an 361
  Copyright terms: Public domain W3C validator