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

Theorem simprll 763
Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)
Assertion
Ref Expression
simprll  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )

Proof of Theorem simprll
StepHypRef Expression
1 simpl 457 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 727 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
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  4434  fcof1  6175  mpt20  6352  eroveu  7408  boxriin  7513  undom  7607  fofinf1o  7803  finsschain  7829  suppeqfsuppbi  7845  fsuppunbi  7852  marypha1lem  7895  wemapsolem  7978  wemapso  7979  wemapso2OLD  7980  wemapso2lem  7981  cantnf  8115  cantnfOLD  8137  iunfictbso  8498  enfin2i  8704  ttukeylem7  8898  fpwwe2lem2  9013  fpwwe2lem9  9019  fpwwe2lem12  9022  fpwwelem  9026  distrlem4pr  9407  mulcmpblnr  9451  prsrlem1  9452  dedekind  9747  divdivdiv  10252  divmuleq  10256  divadddiv  10266  divsubdiv  10267  lediv12a  10445  xmullem  11467  xlemul1a  11491  seqcaopr  12126  leexp2r  12205  hashf1lem1  12486  hashf1lem2  12487  wrd2ind  12685  cshweqrep  12771  lo1le  13456  summolem2  13520  summo  13521  prodmolem2  13724  prodmo  13725  bezoutlem3  14160  bezoutlem4  14161  qredeu  14230  pcadd  14390  prmreclem2  14417  vdwlem9  14489  vdwlem10  14490  ramub1lem2  14527  ramub1  14528  cofucl  15236  setcmon  15393  poslubmo  15755  posglbmo  15756  issubmd  15959  grprcan  16062  isnsg3  16214  ghmpreima  16267  gaorber  16325  psgneu  16510  odcau  16603  lsmsubm  16652  lsmmod  16672  ablfaclem3  17117  ringpropd  17209  lmodvsmmulgdi  17526  lmodprop2d  17551  lss1d  17588  assamulgscmlem2  17977  mplcoe1  18106  mplcoe5  18110  mplcoe2OLD  18112  evlslem1  18163  lindff1  18833  islindf4  18851  mdetunilem7  19098  mdetunilem8  19099  mdetunilem9  19100  mdetuni0  19101  mdetmul  19103  cayhamlem3  19366  ppttop  19486  epttop  19488  cnhaus  19833  isreg2  19856  cncmp  19870  1stcfb  19924  2ndcomap  19937  1stccnp  19941  cldllycmp  19974  1stckgenlem  20032  txcls  20083  ptcnp  20101  txdis1cn  20114  txlly  20115  txnlly  20116  pthaus  20117  txhaus  20126  txkgen  20131  xkohaus  20132  xkococnlem  20138  xkococn  20139  opnfbas  20321  hausflimi  20459  hausflim  20460  hauspwpwf1  20466  alexsubALT  20529  tgpconcomp  20589  qustgplem  20597  metequiv2  20991  met2ndci  21003  nrmmetd  21073  nlmvscnlem1  21173  reconn  21311  xrge0tsms  21317  mulc1cncf  21387  ipcnlem1  21663  minveclem3  21822  pmltpc  21840  ovolicc2lem5  21910  ovolicc2  21911  uniioombllem6  21975  dyadmbllem  21986  vitalilem3  21997  mbfmullem  22110  itg2split  22134  itg2mono  22138  dvlip2  22374  lhop1  22393  dvcnvrelem1  22396  dvfsumrlim  22410  ftc1lem6  22420  itgsubst  22428  dgrco  22650  plyexmo  22687  ulmdvlem3  22775  abelthlem2  22805  abelthlem8  22812  dvdsmulf1o  23448  chpchtsum  23472  dchrptlem2  23518  2sqlem5  23621  2sqlem9  23626  2sqb  23631  chpo1ubb  23644  vmadivsumb  23646  selbergb  23712  selberg2b  23715  selberg3lem2  23721  pntrsumbnd  23729  pntrlog2bnd  23747  pntibndlem3  23755  pnt3  23775  mirreu3  24013  axsegcon  24208  ax5seglem9  24218  axeuclid  24244  axcontlem10  24254  axcontlem12  24256  wwlknredwwlkn0  24705  clwwlkextfrlem1  25054  numclwlk1lem2f1  25072  numclwlk1lem2fo  25073  ablo4  25267  ghgrpOLD  25348  smcnlem  25585  pjhthmo  26198  pjpjpre  26315  lnconi  26930  resf1o  27531  xrge0tsmsd  27753  derangenlem  28593  pconcon  28654  conpcon  28658  cvmfolem  28702  cvmliftmolem2  28705  cvmliftmo  28707  cvmliftlem7  28714  cvmlift2lem10  28735  cvmlift3lem8  28749  linecgr  29707  btwnconn1lem8  29720  btwnconn1lem14  29726  btwnconn3  29729  brsegle  29734  segletr  29740  segleantisym  29741  outsideofeq  29756  linethru  29779  mblfinlem3  30029  bddiblnc  30061  ftc1cnnc  30065  finminlem  30112  nn0prpwlem  30116  neibastop2lem  30154  isbnd3  30256  mzpcl1  30637  mzpcompact2lem  30660  diophin  30682  pell14qrmulcl  30775  pwssplit4  31011  hbtlem2  31049  stoweidlem57  31793  stoweidlem61  31797  fourierdlem92  31935  rabsubmgmd  32433  2zlidl  32567  lmodvsmdi  32845  cvlcvr1  34939  athgt  35055  4atlem12  35211  paddasslem12  35430  paddasslem13  35431  cdleme0cp  35814  cdleme42keg  36087  cdleme42mgN  36089  trlord  36170  cdlemg6c  36221  cdlemkid4  36535  dihopelvalcpre  36850  dihmeetlem1N  36892  dihglblem5apreN  36893  dihmeetlem4preN  36908  dihmeetlem6  36911  dihmeetlem10N  36918  dihmeetlem11N  36919  dihmeetlem13N  36921  dihjatcclem4  37023
  Copyright terms: Public domain W3C validator