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

Theorem simprll 738
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 443 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 708 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  disjxiun  4036  fcof1  5813  mpt20  6215  eroveu  6769  boxriin  6874  undom  6966  fofinf1o  7153  finsschain  7178  marypha1lem  7202  wemapso2lem  7281  wemapso  7282  wemapso2  7283  cantnf  7411  iunfictbso  7757  enfin2i  7963  ttukeylem7  8158  fpwwe2lem2  8270  fpwwe2lem9  8276  fpwwe2lem12  8279  fpwwelem  8283  distrlem4pr  8666  divdivdiv  9477  divmuleq  9481  divadddiv  9491  divsubdiv  9492  lediv12a  9665  xmullem  10600  xlemul1a  10624  seqcaopr  11099  leexp2r  11175  hashf1lem1  11409  hashf1lem2  11410  lo1le  12141  summolem2  12205  summo  12206  bezoutlem3  12735  bezoutlem4  12736  qredeu  12802  pcadd  12953  prmreclem2  12980  vdwlem9  13052  vdwlem10  13053  ramub1lem2  13090  ramub1  13091  cofucl  13778  setcmon  13935  poslubmo  14266  grprcan  14531  isnsg3  14667  ghmpreima  14720  gaorber  14778  odcau  14931  lsmsubm  14980  lsmmod  15000  ablfaclem3  15338  rngpropd  15388  lmodprop2d  15703  lss1d  15736  mplcoe1  16225  mplcoe2  16227  ppttop  16760  epttop  16762  cnhaus  17098  isreg2  17121  cncmp  17135  1stcfb  17187  2ndcomap  17200  1stccnp  17204  cldllycmp  17237  1stckgenlem  17264  txcls  17315  ptcnp  17332  txdis1cn  17345  txlly  17346  txnlly  17347  pthaus  17348  txhaus  17357  txkgen  17362  xkohaus  17363  xkococnlem  17369  xkococn  17370  opnfbas  17553  hausflimi  17691  hausflim  17692  hauspwpwf1  17698  alexsubALT  17761  tgpconcomp  17811  divstgplem  17819  metequiv2  18072  met2ndci  18084  nrmmetd  18113  nlmvscnlem1  18213  reconn  18349  xrge0tsms  18355  mulc1cncf  18425  ipcnlem1  18688  minveclem3  18809  pmltpc  18826  ovolicc2lem5  18896  ovolicc2  18897  uniioombllem6  18959  dyadmbllem  18970  vitalilem3  18981  mbfmullem  19096  itg2split  19120  itg2mono  19124  dvlip2  19358  lhop1  19377  dvcnvrelem1  19380  dvfsumrlim  19394  ftc1lem6  19404  itgsubst  19412  evlslem1  19415  dgrco  19672  plyexmo  19709  ulmdvlem3  19795  abelthlem2  19824  abelthlem8  19831  dvdsmulf1o  20450  chpchtsum  20474  dchrptlem2  20520  2sqlem5  20623  2sqlem9  20628  2sqb  20633  chpo1ubb  20646  vmadivsumb  20648  selbergb  20714  selberg2b  20717  selberg3lem2  20723  pntrsumbnd  20731  pntrlog2bnd  20749  pntibndlem3  20757  pnt3  20777  ablo4  20970  ghgrp  21051  smcnlem  21286  pjhthmo  21897  pjpjpre  22014  lnconi  22629  xrge0tsmsd  23397  derangenlem  23717  pconcon  23777  conpcon  23781  cvmfolem  23825  cvmliftmolem2  23828  cvmliftmo  23830  cvmliftlem7  23837  cvmlift2lem10  23858  cvmlift3lem8  23872  dedekind  24097  prodmolem2  24158  prodmo  24159  axsegcon  24627  ax5seglem9  24637  axeuclid  24663  axcontlem10  24673  axcontlem12  24675  linecgr  24776  btwnconn1lem8  24789  btwnconn1lem14  24795  btwnconn3  24798  brsegle  24803  segletr  24809  segleantisym  24810  outsideofeq  24825  linethru  24848  bddiblnc  25021  ftc1cnnc  25025  resgcom  25454  fprodsub  25482  iintlem1  25713  icccon3  25804  finminlem  26334  nn0prpwlem  26341  neibastop2lem  26412  isbnd3  26611  mzpcl1  26910  mzpcompact2lem  26932  diophin  26955  pell14qrmulcl  27051  pwssplit4  27294  lindff1  27393  islindf4  27411  hbtlem2  27431  issubmd  27486  psgneu  27532  stoweidlem57  27909  stoweidlem61  27913  cvlcvr1  30151  athgt  30267  4atlem12  30423  paddasslem12  30642  paddasslem13  30643  cdleme0cp  31025  cdleme42keg  31297  cdleme42mgN  31299  trlord  31380  cdlemg6c  31431  cdlemkid4  31745  dihopelvalcpre  32060  dihmeetlem1N  32102  dihglblem5apreN  32103  dihmeetlem4preN  32118  dihmeetlem6  32121  dihmeetlem10N  32128  dihmeetlem11N  32129  dihmeetlem13N  32131  dihjatcclem4  32233
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 177  df-an 360
  Copyright terms: Public domain W3C validator