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

Theorem simprlr 773
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 463 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 734 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371
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 189  df-an 373
This theorem is referenced by:  disjxiun  4399  fcof1  6185  fliftfun  6205  wfrlem17  7052  domunfican  7844  finsschain  7881  suppeqfsuppbi  7897  fsuppunbi  7904  wemapsolem  8065  wemapso  8066  wemapso2lem  8067  cantnf  8198  enfin2i  8751  ttukeylem7  8945  fpwwe2lem2  9057  fpwwe2lem9  9063  fpwwe2lem12  9066  fpwwelem  9070  distrlem4pr  9451  mulcmpblnr  9495  prsrlem1  9496  addsrmo  9497  mulsrmo  9498  divdivdiv  10308  divsubdiv  10323  lediv12a  10499  xmullem  11550  xlemul1a  11574  seqcaopr  12250  leexp2r  12330  hashf1lem1  12618  hashf1lem2  12619  fi1uzind  12650  brfi1indALT  12653  wrd2ind  12834  cshweqrep  12920  summolem2  13782  summo  13783  prodmolem2  13989  prodmo  13990  bezoutlem3OLD  14505  bezoutlem4OLD  14506  bezoutlem3  14508  bezoutlem4  14509  qredeu  14664  pcadd  14834  vdwlem9  14939  vdwlem10  14940  ramub1lem2  14985  ramub1  14986  cofucl  15793  setcmon  15982  poslubmo  16392  posglbmo  16393  grprcan  16699  isnsg3  16851  ghmpreima  16904  gaorber  16962  psgneu  17147  odcau  17256  lsmsubm  17305  lsmmod  17325  efgsfo  17389  ablfaclem3  17720  ringpropd  17812  islmodd  18097  lmodprop2d  18150  lss1d  18186  assamulgscmlem2  18573  mplcoe1  18689  mplcoe5  18692  evlslem1  18738  lindff1  19378  islindf4  19396  mdetunilem7  19643  mdetunilem8  19644  mdetunilem9  19645  mdetuni0  19646  mdetmul  19648  ppttop  20022  epttop  20024  cnhaus  20370  isreg2  20393  cncmp  20407  1stcfb  20460  2ndcomap  20473  cldllycmp  20510  txcls  20619  ptclsg  20630  ptcnp  20637  txdis1cn  20650  txlly  20651  txnlly  20652  pthaus  20653  txhaus  20662  txkgen  20667  xkohaus  20668  xkococnlem  20674  xkococn  20675  fgabs  20894  rnelfm  20968  hausflimi  20995  hausflim  20996  alexsubALTlem2  21063  alexsubALTlem4  21065  alexsubALT  21066  tgpconcomp  21127  qustgplem  21135  metequiv2  21525  met2ndci  21537  nrmmetd  21589  nlmvscnlem1  21689  reconn  21846  xrge0tsms  21852  ipcnlem1  22216  minveclem3  22371  minveclem3OLD  22383  pmltpc  22401  ovolicc2lem5  22475  ovolicc2  22476  uniioombllem6  22546  dyadmbllem  22557  vitalilem3  22568  mbfmullem  22683  itg2split  22707  itg2mono  22711  dvlip2  22947  lhop1  22966  dvcnvrelem1  22969  ftc1lem6  22993  itgsubst  23001  dgrco  23229  plyexmo  23266  ulmdvlem3  23357  abelthlem2  23387  abelthlem8  23394  dvdsmulf1o  24123  chpchtsum  24147  dchrptlem2  24193  2sqlem5  24296  2sqlem9  24301  2sqb  24306  pntrlog2bnd  24422  pntibndlem3  24430  pntlemp  24448  pnt3  24450  hlcgreu  24663  mirreu3  24699  cgraswap  24862  cgracom  24864  cgratr  24865  acopyeu  24875  axsegcon  24957  ax5seglem9  24967  axeuclid  24993  axcontlem12  25005  clwwlkf1  25524  wwlkext2clwwlk  25531  frgranbnb  25748  ablo4  26015  ghgrpOLD  26096  smcnlem  26333  pjhthmo  26955  pjpjpre  27072  3oalem2  27316  lnconi  27686  atom1d  28006  resf1o  28315  xrge0tsmsd  28548  ballotlemfc0  29325  ballotlemfcc  29326  pconcon  29954  cvmfolem  30002  cvmliftmo  30007  cvmliftlem7  30014  cvmlift2lem10  30035  cvmlift3lem8  30049  lineext  30843  linecgr  30848  btwnconn1lem10  30863  btwnconn1lem11  30864  btwnconn3  30870  brsegle  30875  seglecgr12im  30877  segleantisym  30882  outsideoftr  30896  outsideofeq  30897  outsideofeu  30898  linethru  30920  finminlem  30974  neibastop2lem  31016  isbasisrelowllem1  31758  isbasisrelowllem2  31759  mblfinlem3  31979  bddiblnc  32012  ftc1cnnc  32016  isbnd3  32116  heibor1lem  32141  crngm4  32236  cvlcvr1  32905  4atlem12  33177  paddasslem12  33396  paddasslem13  33397  lhpexle2lem  33574  trlord  34136  cdlemkid4  34501  dihopelvalcpre  34816  dihmeetlem1N  34858  dihglblem5apreN  34859  dihmeetlem6  34877  dih1dimatlem0  34896  dihjatcclem4  34989  mzpcl2  35572  mzpmfp  35589  mzpcompact2lem  35593  diophin  35615  pell14qrmulcl  35709  hbtlem2  35983  iunrelexpuztr  36311  stoweidlem61  37922  fourierdlem92  38062  snlindsntor  40317  elfzolborelfzop1  40369  nn0sumshdiglemB  40484
  Copyright terms: Public domain W3C validator