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

Theorem simprll 754
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 454 . 2  |-  ( ( ps  /\  ch )  ->  ps )
21ad2antrl 720 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  4277  fcof1  5978  mpt20  6145  eroveu  7183  boxriin  7293  undom  7387  fofinf1o  7580  finsschain  7606  suppeqfsuppbi  7622  fsuppunbi  7629  marypha1lem  7671  wemapsolem  7752  wemapso  7753  wemapso2OLD  7754  wemapso2lem  7755  cantnf  7889  cantnfOLD  7911  iunfictbso  8272  enfin2i  8478  ttukeylem7  8672  fpwwe2lem2  8786  fpwwe2lem9  8792  fpwwe2lem12  8795  fpwwelem  8799  distrlem4pr  9182  dedekind  9520  divdivdiv  10019  divmuleq  10023  divadddiv  10033  divsubdiv  10034  lediv12a  10212  xmullem  11214  xlemul1a  11238  seqcaopr  11826  leexp2r  11904  hashf1lem1  12191  hashf1lem2  12192  wrd2ind  12355  cshweqrep  12438  lo1le  13112  summolem2  13176  summo  13177  bezoutlem3  13706  bezoutlem4  13707  qredeu  13775  pcadd  13933  prmreclem2  13960  vdwlem9  14032  vdwlem10  14033  ramub1lem2  14070  ramub1  14071  cofucl  14780  setcmon  14937  poslubmo  15298  posglbmo  15299  issubmd  15458  grprcan  15550  isnsg3  15694  ghmpreima  15747  gaorber  15805  psgneu  15991  odcau  16082  lsmsubm  16131  lsmmod  16151  ablfaclem3  16561  rngpropd  16611  lmodprop2d  16930  lss1d  16965  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  lindff1  18090  islindf4  18108  mdetunilem7  18265  mdetunilem8  18266  mdetunilem9  18267  mdetuni0  18268  mdetmul  18270  ppttop  18452  epttop  18454  cnhaus  18799  isreg2  18822  cncmp  18836  1stcfb  18890  2ndcomap  18903  1stccnp  18907  cldllycmp  18940  1stckgenlem  18967  txcls  19018  ptcnp  19036  txdis1cn  19049  txlly  19050  txnlly  19051  pthaus  19052  txhaus  19061  txkgen  19066  xkohaus  19067  xkococnlem  19073  xkococn  19074  opnfbas  19256  hausflimi  19394  hausflim  19395  hauspwpwf1  19401  alexsubALT  19464  tgpconcomp  19524  divstgplem  19532  metequiv2  19926  met2ndci  19938  nrmmetd  20008  nlmvscnlem1  20108  reconn  20246  xrge0tsms  20252  mulc1cncf  20322  ipcnlem1  20598  minveclem3  20757  pmltpc  20775  ovolicc2lem5  20845  ovolicc2  20846  uniioombllem6  20909  dyadmbllem  20920  vitalilem3  20931  mbfmullem  21044  itg2split  21068  itg2mono  21072  dvlip2  21308  lhop1  21327  dvcnvrelem1  21330  dvfsumrlim  21344  ftc1lem6  21354  itgsubst  21362  evlslem1  21366  dgrco  21626  plyexmo  21663  ulmdvlem3  21751  abelthlem2  21781  abelthlem8  21788  dvdsmulf1o  22418  chpchtsum  22442  dchrptlem2  22488  2sqlem5  22591  2sqlem9  22596  2sqb  22601  chpo1ubb  22614  vmadivsumb  22616  selbergb  22682  selberg2b  22685  selberg3lem2  22691  pntrsumbnd  22699  pntrlog2bnd  22717  pntibndlem3  22725  pnt3  22745  mirreu3  22923  axsegcon  22995  ax5seglem9  23005  axeuclid  23031  axcontlem10  23041  axcontlem12  23043  ablo4  23596  ghgrp  23677  smcnlem  23914  pjhthmo  24527  pjpjpre  24644  lnconi  25259  resf1o  25854  xrge0tsmsd  26105  derangenlem  26906  pconcon  26967  conpcon  26971  cvmfolem  27015  cvmliftmolem2  27018  cvmliftmo  27020  cvmliftlem7  27027  cvmlift2lem10  27048  cvmlift3lem8  27062  prodmolem2  27294  prodmo  27295  linecgr  27958  btwnconn1lem8  27971  btwnconn1lem14  27977  btwnconn3  27980  brsegle  27985  segletr  27991  segleantisym  27992  outsideofeq  28007  linethru  28030  mblfinlem3  28271  bddiblnc  28303  ftc1cnnc  28307  finminlem  28354  nn0prpwlem  28358  neibastop2lem  28422  isbnd3  28524  mzpcl1  28907  mzpcompact2lem  28930  diophin  28953  pell14qrmulcl  29046  pwssplit4  29284  hbtlem2  29322  stoweidlem57  29695  stoweidlem61  29699  wwlknredwwlkn0  30202  clwwlkextfrlem1  30512  numclwlk1lem2f1  30530  numclwlk1lem2fo  30531  cvlcvr1  32554  athgt  32670  4atlem12  32826  paddasslem12  33045  paddasslem13  33046  cdleme0cp  33428  cdleme42keg  33700  cdleme42mgN  33702  trlord  33783  cdlemg6c  33834  cdlemkid4  34148  dihopelvalcpre  34463  dihmeetlem1N  34505  dihglblem5apreN  34506  dihmeetlem4preN  34521  dihmeetlem6  34524  dihmeetlem10N  34531  dihmeetlem11N  34532  dihmeetlem13N  34534  dihjatcclem4  34636
  Copyright terms: Public domain W3C validator