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

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

Proof of Theorem simprlr
StepHypRef Expression
1 simpr 447 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 708 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  disjxiun  4099  fcof1  5881  fliftfun  5895  domunfican  7216  finsschain  7249  wemapso2lem  7352  wemapso  7353  wemapso2  7354  cantnf  7482  enfin2i  8034  ttukeylem7  8229  fpwwe2lem2  8341  fpwwe2lem9  8347  fpwwe2lem12  8350  fpwwelem  8354  distrlem4pr  8737  divdivdiv  9548  divsubdiv  9563  lediv12a  9736  xmullem  10673  xlemul1a  10697  seqcaopr  11172  leexp2r  11249  hashf1lem1  11483  hashf1lem2  11484  summolem2  12280  summo  12281  bezoutlem3  12810  bezoutlem4  12811  qredeu  12877  pcadd  13028  vdwlem9  13127  vdwlem10  13128  ramub1lem2  13165  ramub1  13166  cofucl  13855  setcmon  14012  poslubmo  14343  grprcan  14608  isnsg3  14744  ghmpreima  14797  gaorber  14855  odcau  15008  lsmsubm  15057  lsmmod  15077  efgsfo  15141  ablfaclem3  15415  rngpropd  15465  islmodd  15726  lmodprop2d  15780  lss1d  15813  mplcoe1  16302  mplcoe2  16304  ppttop  16844  epttop  16846  cnhaus  17182  isreg2  17205  cncmp  17219  1stcfb  17271  2ndcomap  17284  cldllycmp  17321  txcls  17399  ptclsg  17409  ptcnp  17416  txdis1cn  17429  txlly  17430  txnlly  17431  pthaus  17432  txhaus  17441  txkgen  17446  xkohaus  17447  xkococnlem  17453  xkococn  17454  fgabs  17670  rnelfm  17744  hausflimi  17771  hausflim  17772  alexsubALTlem2  17838  alexsubALTlem4  17840  alexsubALT  17841  tgpconcomp  17891  divstgplem  17899  metequiv2  18152  met2ndci  18164  nrmmetd  18193  nlmvscnlem1  18293  reconn  18430  xrge0tsms  18436  ipcnlem1  18770  minveclem3  18891  pmltpc  18908  ovolicc2lem5  18978  ovolicc2  18979  uniioombllem6  19041  dyadmbllem  19052  vitalilem3  19063  mbfmullem  19178  itg2split  19202  itg2mono  19206  dvlip2  19440  lhop1  19459  dvcnvrelem1  19462  ftc1lem6  19486  itgsubst  19494  evlslem1  19497  dgrco  19754  plyexmo  19791  ulmdvlem3  19879  abelthlem2  19909  abelthlem8  19916  dvdsmulf1o  20540  chpchtsum  20564  dchrptlem2  20610  2sqlem5  20713  2sqlem9  20718  2sqb  20723  pntrlog2bnd  20839  pntibndlem3  20847  pntlemp  20865  pnt3  20867  ablo4  21060  ghgrp  21141  smcnlem  21378  pjhthmo  21989  pjpjpre  22106  3oalem2  22350  lnconi  22721  atom1d  23041  xrge0tsmsd  23415  ballotlemfc0  23999  ballotlemfcc  24000  pconcon  24166  cvmfolem  24214  cvmliftmo  24219  cvmliftlem7  24226  cvmlift2lem10  24247  cvmlift3lem8  24261  prodmolem2  24562  prodmo  24563  axsegcon  25114  ax5seglem9  25124  axeuclid  25150  axcontlem12  25162  lineext  25258  linecgr  25263  btwnconn1lem10  25278  btwnconn1lem11  25279  btwnconn3  25285  brsegle  25290  seglecgr12im  25292  segleantisym  25297  outsideoftr  25311  outsideofeq  25312  outsideofeu  25313  linethru  25335  itg2addnc  25494  bddiblnc  25510  ftc1cnnc  25514  finminlem  25555  neibastop2lem  25633  isbnd3  25831  heibor1lem  25856  crngm4  25951  mzpcl2  26131  mzpmfp  26148  mzpcompact2lem  26152  diophin  26175  pell14qrmulcl  26271  lindff1  26613  islindf4  26631  hbtlem2  26651  psgneu  26752  brfi1uzind  27489  cvlcvr1  29581  4atlem12  29853  paddasslem12  30072  paddasslem13  30073  lhpexle2lem  30250  trlord  30810  cdlemkid4  31175  dihopelvalcpre  31490  dihmeetlem1N  31532  dihglblem5apreN  31533  dihmeetlem6  31551  dih1dimatlem0  31570  dihjatcclem4  31663
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