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

Theorem simprll 770
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 458 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 732 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  disjxiun  4417  fcof1  6196  mpt20  6371  wfrlem17  7056  eroveu  7462  boxriin  7568  undom  7662  fofinf1o  7854  finsschain  7883  suppeqfsuppbi  7899  fsuppunbi  7906  marypha1lem  7949  wemapsolem  8067  wemapso  8068  wemapso2lem  8069  cantnf  8199  iunfictbso  8545  enfin2i  8751  ttukeylem7  8945  fpwwe2lem2  9057  fpwwe2lem9  9063  fpwwe2lem12  9066  fpwwelem  9070  distrlem4pr  9451  mulcmpblnr  9495  prsrlem1  9496  dedekind  9797  divdivdiv  10308  divmuleq  10312  divadddiv  10322  divsubdiv  10323  lediv12a  10499  xmullem  11550  xlemul1a  11574  seqcaopr  12249  leexp2r  12329  hashf1lem1  12615  hashf1lem2  12616  wrd2ind  12822  cshweqrep  12908  lo1le  13700  summolem2  13767  summo  13768  prodmolem2  13974  prodmo  13975  bezoutlem3OLD  14490  bezoutlem4OLD  14491  bezoutlem3  14493  bezoutlem4  14494  qredeu  14649  pcadd  14819  prmreclem2  14846  vdwlem9  14924  vdwlem10  14925  ramub1lem2  14970  ramub1  14971  prmgaplem7  15012  cofucl  15778  setcmon  15967  poslubmo  16377  posglbmo  16378  issubmd  16581  grprcan  16684  isnsg3  16836  ghmpreima  16889  gaorber  16947  psgneu  17132  odcau  17241  lsmsubm  17290  lsmmod  17310  ablfaclem3  17705  ringpropd  17797  lmodvsmmulgdi  18111  lmodprop2d  18135  lss1d  18171  assamulgscmlem2  18558  mplcoe1  18674  mplcoe5  18677  evlslem1  18723  lindff1  19362  islindf4  19380  mdetunilem7  19627  mdetunilem8  19628  mdetunilem9  19629  mdetuni0  19630  mdetmul  19632  cayhamlem3  19895  ppttop  20006  epttop  20008  cnhaus  20354  isreg2  20377  cncmp  20391  1stcfb  20444  2ndcomap  20457  1stccnp  20461  cldllycmp  20494  1stckgenlem  20552  txcls  20603  ptcnp  20621  txdis1cn  20634  txlly  20635  txnlly  20636  pthaus  20637  txhaus  20646  txkgen  20651  xkohaus  20652  xkococnlem  20658  xkococn  20659  opnfbas  20841  hausflimi  20979  hausflim  20980  hauspwpwf1  20986  alexsubALT  21050  tgpconcomp  21111  qustgplem  21119  metequiv2  21509  met2ndci  21521  nrmmetd  21573  nlmvscnlem1  21673  reconn  21830  xrge0tsms  21836  mulc1cncf  21921  ipcnlem1  22200  minveclem3  22355  minveclem3OLD  22367  pmltpc  22385  ovolicc2lem5  22459  ovolicc2  22460  uniioombllem6  22530  dyadmbllem  22541  vitalilem3  22552  mbfmullem  22667  itg2split  22691  itg2mono  22695  dvlip2  22931  lhop1  22950  dvcnvrelem1  22953  dvfsumrlim  22967  ftc1lem6  22977  itgsubst  22985  dgrco  23213  plyexmo  23250  ulmdvlem3  23341  abelthlem2  23371  abelthlem8  23378  dvdsmulf1o  24107  chpchtsum  24131  dchrptlem2  24177  2sqlem5  24280  2sqlem9  24285  2sqb  24290  chpo1ubb  24303  vmadivsumb  24305  selbergb  24371  selberg2b  24374  selberg3lem2  24380  pntrsumbnd  24388  pntrlog2bnd  24406  pntibndlem3  24414  pnt3  24434  hlcgreu  24647  mirreu3  24683  cgraswap  24846  cgracom  24848  cgratr  24849  acopyeu  24859  axsegcon  24941  ax5seglem9  24951  axeuclid  24977  axcontlem10  24987  axcontlem12  24989  wwlknredwwlkn0  25438  clwwlkextfrlem1  25787  numclwlk1lem2f1  25805  numclwlk1lem2fo  25806  ablo4  25998  ghgrpOLD  26079  smcnlem  26316  pjhthmo  26938  pjpjpre  27055  lnconi  27669  resf1o  28306  xrge0tsmsd  28541  derangenlem  29887  pconcon  29947  conpcon  29951  cvmfolem  29995  cvmliftmolem2  29998  cvmliftmo  30000  cvmliftlem7  30007  cvmlift2lem10  30028  cvmlift3lem8  30042  linecgr  30838  btwnconn1lem8  30851  btwnconn1lem14  30857  btwnconn3  30860  brsegle  30865  segletr  30871  segleantisym  30872  outsideofeq  30887  linethru  30910  finminlem  30964  nn0prpwlem  30968  neibastop2lem  31006  mblfinlem3  31890  bddiblnc  31923  ftc1cnnc  31927  isbnd3  32027  cvlcvr1  32821  athgt  32937  4atlem12  33093  paddasslem12  33312  paddasslem13  33313  cdleme0cp  33696  cdleme42keg  33969  cdleme42mgN  33971  trlord  34052  cdlemg6c  34103  cdlemkid4  34417  dihopelvalcpre  34732  dihmeetlem1N  34774  dihglblem5apreN  34775  dihmeetlem4preN  34790  dihmeetlem6  34793  dihmeetlem10N  34800  dihmeetlem11N  34801  dihmeetlem13N  34803  dihjatcclem4  34905  mzpcl1  35487  mzpcompact2lem  35509  diophin  35531  pell14qrmulcl  35626  pwssplit4  35864  hbtlem2  35900  iunrelexpuztr  36168  stoweidlem57  37735  stoweidlem61  37739  fourierdlem92  37879  rabsubmgmd  38977  2zlidl  39120  lmodvsmdi  39355
  Copyright terms: Public domain W3C validator