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

Theorem simprll 761
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  4284  fcof1  5986  mpt20  6151  eroveu  7187  boxriin  7297  undom  7391  fofinf1o  7584  finsschain  7610  suppeqfsuppbi  7626  fsuppunbi  7633  marypha1lem  7675  wemapsolem  7756  wemapso  7757  wemapso2OLD  7758  wemapso2lem  7759  cantnf  7893  cantnfOLD  7915  iunfictbso  8276  enfin2i  8482  ttukeylem7  8676  fpwwe2lem2  8791  fpwwe2lem9  8797  fpwwe2lem12  8800  fpwwelem  8804  distrlem4pr  9187  dedekind  9525  divdivdiv  10024  divmuleq  10028  divadddiv  10038  divsubdiv  10039  lediv12a  10217  xmullem  11219  xlemul1a  11243  seqcaopr  11835  leexp2r  11913  hashf1lem1  12200  hashf1lem2  12201  wrd2ind  12364  cshweqrep  12447  lo1le  13121  summolem2  13185  summo  13186  bezoutlem3  13716  bezoutlem4  13717  qredeu  13785  pcadd  13943  prmreclem2  13970  vdwlem9  14042  vdwlem10  14043  ramub1lem2  14080  ramub1  14081  cofucl  14790  setcmon  14947  poslubmo  15308  posglbmo  15309  issubmd  15468  grprcan  15562  isnsg3  15706  ghmpreima  15759  gaorber  15817  psgneu  16003  odcau  16094  lsmsubm  16143  lsmmod  16163  ablfaclem3  16576  rngpropd  16664  lmodprop2d  16985  lss1d  17021  mplcoe1  17521  mplcoe2  17524  mplcoe2OLD  17525  evlslem1  17576  lindff1  18224  islindf4  18242  mdetunilem7  18399  mdetunilem8  18400  mdetunilem9  18401  mdetuni0  18402  mdetmul  18404  ppttop  18586  epttop  18588  cnhaus  18933  isreg2  18956  cncmp  18970  1stcfb  19024  2ndcomap  19037  1stccnp  19041  cldllycmp  19074  1stckgenlem  19101  txcls  19152  ptcnp  19170  txdis1cn  19183  txlly  19184  txnlly  19185  pthaus  19186  txhaus  19195  txkgen  19200  xkohaus  19201  xkococnlem  19207  xkococn  19208  opnfbas  19390  hausflimi  19528  hausflim  19529  hauspwpwf1  19535  alexsubALT  19598  tgpconcomp  19658  divstgplem  19666  metequiv2  20060  met2ndci  20072  nrmmetd  20142  nlmvscnlem1  20242  reconn  20380  xrge0tsms  20386  mulc1cncf  20456  ipcnlem1  20732  minveclem3  20891  pmltpc  20909  ovolicc2lem5  20979  ovolicc2  20980  uniioombllem6  21043  dyadmbllem  21054  vitalilem3  21065  mbfmullem  21178  itg2split  21202  itg2mono  21206  dvlip2  21442  lhop1  21461  dvcnvrelem1  21464  dvfsumrlim  21478  ftc1lem6  21488  itgsubst  21496  dgrco  21717  plyexmo  21754  ulmdvlem3  21842  abelthlem2  21872  abelthlem8  21879  dvdsmulf1o  22509  chpchtsum  22533  dchrptlem2  22579  2sqlem5  22682  2sqlem9  22687  2sqb  22692  chpo1ubb  22705  vmadivsumb  22707  selbergb  22773  selberg2b  22776  selberg3lem2  22782  pntrsumbnd  22790  pntrlog2bnd  22808  pntibndlem3  22816  pnt3  22836  mirreu3  23026  axsegcon  23124  ax5seglem9  23134  axeuclid  23160  axcontlem10  23170  axcontlem12  23172  ablo4  23725  ghgrp  23806  smcnlem  24043  pjhthmo  24656  pjpjpre  24773  lnconi  25388  resf1o  25981  xrge0tsmsd  26204  derangenlem  27011  pconcon  27072  conpcon  27076  cvmfolem  27120  cvmliftmolem2  27123  cvmliftmo  27125  cvmliftlem7  27132  cvmlift2lem10  27153  cvmlift3lem8  27167  prodmolem2  27399  prodmo  27400  linecgr  28063  btwnconn1lem8  28076  btwnconn1lem14  28082  btwnconn3  28085  brsegle  28090  segletr  28096  segleantisym  28097  outsideofeq  28112  linethru  28135  mblfinlem3  28383  bddiblnc  28415  ftc1cnnc  28419  finminlem  28466  nn0prpwlem  28470  neibastop2lem  28534  isbnd3  28636  mzpcl1  29018  mzpcompact2lem  29041  diophin  29064  pell14qrmulcl  29157  pwssplit4  29395  hbtlem2  29433  stoweidlem57  29805  stoweidlem61  29809  wwlknredwwlkn0  30312  clwwlkextfrlem1  30622  numclwlk1lem2f1  30640  numclwlk1lem2fo  30641  lmodvsmdi  30751  lmodvsmmulgdi  30752  assamulgscmlem2  30760  cvlcvr1  32824  athgt  32940  4atlem12  33096  paddasslem12  33315  paddasslem13  33316  cdleme0cp  33698  cdleme42keg  33970  cdleme42mgN  33972  trlord  34053  cdlemg6c  34104  cdlemkid4  34418  dihopelvalcpre  34733  dihmeetlem1N  34775  dihglblem5apreN  34776  dihmeetlem4preN  34791  dihmeetlem6  34794  dihmeetlem10N  34801  dihmeetlem11N  34802  dihmeetlem13N  34804  dihjatcclem4  34906
  Copyright terms: Public domain W3C validator