MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprlr Structured version   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  4209  fcof1  6020  fliftfun  6034  domunfican  7379  finsschain  7413  wemapso2lem  7519  wemapso  7520  wemapso2  7521  cantnf  7649  enfin2i  8201  ttukeylem7  8395  fpwwe2lem2  8507  fpwwe2lem9  8513  fpwwe2lem12  8516  fpwwelem  8520  distrlem4pr  8903  divdivdiv  9715  divsubdiv  9730  lediv12a  9903  xmullem  10843  xlemul1a  10867  seqcaopr  11360  leexp2r  11437  hashf1lem1  11704  hashf1lem2  11705  brfi1uzind  11715  summolem2  12510  summo  12511  bezoutlem3  13040  bezoutlem4  13041  qredeu  13107  pcadd  13258  vdwlem9  13357  vdwlem10  13358  ramub1lem2  13395  ramub1  13396  cofucl  14085  setcmon  14242  poslubmo  14573  grprcan  14838  isnsg3  14974  ghmpreima  15027  gaorber  15085  odcau  15238  lsmsubm  15287  lsmmod  15307  efgsfo  15371  ablfaclem3  15645  rngpropd  15695  islmodd  15956  lmodprop2d  16006  lss1d  16039  mplcoe1  16528  mplcoe2  16530  ppttop  17071  epttop  17073  cnhaus  17418  isreg2  17441  cncmp  17455  1stcfb  17508  2ndcomap  17521  cldllycmp  17558  txcls  17636  ptclsg  17647  ptcnp  17654  txdis1cn  17667  txlly  17668  txnlly  17669  pthaus  17670  txhaus  17679  txkgen  17684  xkohaus  17685  xkococnlem  17691  xkococn  17692  fgabs  17911  rnelfm  17985  hausflimi  18012  hausflim  18013  alexsubALTlem2  18079  alexsubALTlem4  18081  alexsubALT  18082  tgpconcomp  18142  divstgplem  18150  metequiv2  18540  met2ndci  18552  nrmmetd  18622  nlmvscnlem1  18722  reconn  18859  xrge0tsms  18865  ipcnlem1  19199  minveclem3  19330  pmltpc  19347  ovolicc2lem5  19417  ovolicc2  19418  uniioombllem6  19480  dyadmbllem  19491  vitalilem3  19502  mbfmullem  19617  itg2split  19641  itg2mono  19645  dvlip2  19879  lhop1  19898  dvcnvrelem1  19901  ftc1lem6  19925  itgsubst  19933  evlslem1  19936  dgrco  20193  plyexmo  20230  ulmdvlem3  20318  abelthlem2  20348  abelthlem8  20355  dvdsmulf1o  20979  chpchtsum  21003  dchrptlem2  21049  2sqlem5  21152  2sqlem9  21157  2sqb  21162  pntrlog2bnd  21278  pntibndlem3  21286  pntlemp  21304  pnt3  21306  ablo4  21875  ghgrp  21956  smcnlem  22193  pjhthmo  22804  pjpjpre  22921  3oalem2  23165  lnconi  23536  atom1d  23856  xrge0tsmsd  24223  ballotlemfc0  24750  ballotlemfcc  24751  pconcon  24918  cvmfolem  24966  cvmliftmo  24971  cvmliftlem7  24978  cvmlift2lem10  24999  cvmlift3lem8  25013  prodmolem2  25261  prodmo  25262  axsegcon  25866  ax5seglem9  25876  axeuclid  25902  axcontlem12  25914  lineext  26010  linecgr  26015  btwnconn1lem10  26030  btwnconn1lem11  26031  btwnconn3  26037  brsegle  26042  seglecgr12im  26044  segleantisym  26049  outsideoftr  26063  outsideofeq  26064  outsideofeu  26065  linethru  26087  mblfinlem3  26245  bddiblnc  26275  ftc1cnnc  26279  finminlem  26321  neibastop2lem  26389  isbnd3  26493  heibor1lem  26518  crngm4  26613  mzpcl2  26787  mzpmfp  26804  mzpcompact2lem  26808  diophin  26831  pell14qrmulcl  26926  lindff1  27267  islindf4  27285  hbtlem2  27305  psgneu  27406  stoweidlem61  27786  frgranbnb  28410  cvlcvr1  30137  4atlem12  30409  paddasslem12  30628  paddasslem13  30629  lhpexle2lem  30806  trlord  31366  cdlemkid4  31731  dihopelvalcpre  32046  dihmeetlem1N  32088  dihglblem5apreN  32089  dihmeetlem6  32107  dih1dimatlem0  32126  dihjatcclem4  32219
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