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

Theorem simprlr 741
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 449 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 710 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  disjxiun  4212  fcof1  6023  fliftfun  6037  domunfican  7382  finsschain  7416  wemapso2lem  7522  wemapso  7523  wemapso2  7524  cantnf  7652  enfin2i  8206  ttukeylem7  8400  fpwwe2lem2  8512  fpwwe2lem9  8518  fpwwe2lem12  8521  fpwwelem  8525  distrlem4pr  8908  divdivdiv  9720  divsubdiv  9735  lediv12a  9908  xmullem  10848  xlemul1a  10872  seqcaopr  11365  leexp2r  11442  hashf1lem1  11709  hashf1lem2  11710  brfi1uzind  11720  summolem2  12515  summo  12516  bezoutlem3  13045  bezoutlem4  13046  qredeu  13112  pcadd  13263  vdwlem9  13362  vdwlem10  13363  ramub1lem2  13400  ramub1  13401  cofucl  14090  setcmon  14247  poslubmo  14578  grprcan  14843  isnsg3  14979  ghmpreima  15032  gaorber  15090  odcau  15243  lsmsubm  15292  lsmmod  15312  efgsfo  15376  ablfaclem3  15650  rngpropd  15700  islmodd  15961  lmodprop2d  16011  lss1d  16044  mplcoe1  16533  mplcoe2  16535  ppttop  17076  epttop  17078  cnhaus  17423  isreg2  17446  cncmp  17460  1stcfb  17513  2ndcomap  17526  cldllycmp  17563  txcls  17641  ptclsg  17652  ptcnp  17659  txdis1cn  17672  txlly  17673  txnlly  17674  pthaus  17675  txhaus  17684  txkgen  17689  xkohaus  17690  xkococnlem  17696  xkococn  17697  fgabs  17916  rnelfm  17990  hausflimi  18017  hausflim  18018  alexsubALTlem2  18084  alexsubALTlem4  18086  alexsubALT  18087  tgpconcomp  18147  divstgplem  18155  metequiv2  18545  met2ndci  18557  nrmmetd  18627  nlmvscnlem1  18727  reconn  18864  xrge0tsms  18870  ipcnlem1  19204  minveclem3  19335  pmltpc  19352  ovolicc2lem5  19422  ovolicc2  19423  uniioombllem6  19485  dyadmbllem  19496  vitalilem3  19507  mbfmullem  19620  itg2split  19644  itg2mono  19648  dvlip2  19884  lhop1  19903  dvcnvrelem1  19906  ftc1lem6  19930  itgsubst  19938  evlslem1  19941  dgrco  20198  plyexmo  20235  ulmdvlem3  20323  abelthlem2  20353  abelthlem8  20360  dvdsmulf1o  20984  chpchtsum  21008  dchrptlem2  21054  2sqlem5  21157  2sqlem9  21162  2sqb  21167  pntrlog2bnd  21283  pntibndlem3  21291  pntlemp  21309  pnt3  21311  ablo4  21880  ghgrp  21961  smcnlem  22198  pjhthmo  22809  pjpjpre  22926  3oalem2  23170  lnconi  23541  atom1d  23861  xrge0tsmsd  24228  ballotlemfc0  24755  ballotlemfcc  24756  pconcon  24923  cvmfolem  24971  cvmliftmo  24976  cvmliftlem7  24983  cvmlift2lem10  25004  cvmlift3lem8  25018  prodmolem2  25266  prodmo  25267  axsegcon  25871  ax5seglem9  25881  axeuclid  25907  axcontlem12  25919  lineext  26015  linecgr  26020  btwnconn1lem10  26035  btwnconn1lem11  26036  btwnconn3  26042  brsegle  26047  seglecgr12im  26049  segleantisym  26054  outsideoftr  26068  outsideofeq  26069  outsideofeu  26070  linethru  26092  mblfinlem3  26257  bddiblnc  26289  ftc1cnnc  26293  finminlem  26335  neibastop2lem  26403  isbnd3  26507  heibor1lem  26532  crngm4  26627  mzpcl2  26801  mzpmfp  26818  mzpcompact2lem  26822  diophin  26845  pell14qrmulcl  26940  lindff1  27281  islindf4  27299  hbtlem2  27319  psgneu  27420  stoweidlem61  27800  frgranbnb  28484  cvlcvr1  30211  4atlem12  30483  paddasslem12  30702  paddasslem13  30703  lhpexle2lem  30880  trlord  31440  cdlemkid4  31805  dihopelvalcpre  32120  dihmeetlem1N  32162  dihglblem5apreN  32163  dihmeetlem6  32181  dih1dimatlem0  32200  dihjatcclem4  32293
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 179  df-an 362
  Copyright terms: Public domain W3C validator