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

Theorem simprlr 762
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 459 . 2  |-  ( ( ps  /\  ch )  ->  ch )
21ad2antrl 725 1  |-  ( (
ph  /\  ( ( ps  /\  ch )  /\  th ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 369
This theorem is referenced by:  disjxiun  4436  fcof1  6165  fliftfun  6185  domunfican  7785  finsschain  7819  suppeqfsuppbi  7835  fsuppunbi  7842  wemapsolem  7967  wemapso  7968  wemapso2OLD  7969  wemapso2lem  7970  cantnf  8103  cantnfOLD  8125  enfin2i  8692  ttukeylem7  8886  fpwwe2lem2  8999  fpwwe2lem9  9005  fpwwe2lem12  9008  fpwwelem  9012  distrlem4pr  9393  mulcmpblnr  9437  prsrlem1  9438  addsrmo  9439  mulsrmo  9440  divdivdiv  10241  divsubdiv  10256  lediv12a  10433  xmullem  11459  xlemul1a  11483  seqcaopr  12129  leexp2r  12208  hashf1lem1  12491  hashf1lem2  12492  brfi1uzind  12519  wrd2ind  12697  cshweqrep  12783  summolem2  13623  summo  13624  prodmolem2  13827  prodmo  13828  bezoutlem3  14265  bezoutlem4  14266  qredeu  14335  pcadd  14495  vdwlem9  14594  vdwlem10  14595  ramub1lem2  14632  ramub1  14633  cofucl  15379  setcmon  15568  poslubmo  15978  posglbmo  15979  grprcan  16285  isnsg3  16437  ghmpreima  16490  gaorber  16548  psgneu  16733  odcau  16826  lsmsubm  16875  lsmmod  16895  efgsfo  16959  ablfaclem3  17336  ringpropd  17428  islmodd  17716  lmodprop2d  17770  lss1d  17807  assamulgscmlem2  18196  mplcoe1  18325  mplcoe5  18329  mplcoe2OLD  18331  evlslem1  18382  lindff1  19025  islindf4  19043  mdetunilem7  19290  mdetunilem8  19291  mdetunilem9  19292  mdetuni0  19293  mdetmul  19295  ppttop  19678  epttop  19680  cnhaus  20025  isreg2  20048  cncmp  20062  1stcfb  20115  2ndcomap  20128  cldllycmp  20165  txcls  20274  ptclsg  20285  ptcnp  20292  txdis1cn  20305  txlly  20306  txnlly  20307  pthaus  20308  txhaus  20317  txkgen  20322  xkohaus  20323  xkococnlem  20329  xkococn  20330  fgabs  20549  rnelfm  20623  hausflimi  20650  hausflim  20651  alexsubALTlem2  20717  alexsubALTlem4  20719  alexsubALT  20720  tgpconcomp  20780  qustgplem  20788  metequiv2  21182  met2ndci  21194  nrmmetd  21264  nlmvscnlem1  21364  reconn  21502  xrge0tsms  21508  ipcnlem1  21854  minveclem3  22013  pmltpc  22031  ovolicc2lem5  22101  ovolicc2  22102  uniioombllem6  22166  dyadmbllem  22177  vitalilem3  22188  mbfmullem  22301  itg2split  22325  itg2mono  22329  dvlip2  22565  lhop1  22584  dvcnvrelem1  22587  ftc1lem6  22611  itgsubst  22619  dgrco  22841  plyexmo  22878  ulmdvlem3  22966  abelthlem2  22996  abelthlem8  23003  dvdsmulf1o  23671  chpchtsum  23695  dchrptlem2  23741  2sqlem5  23844  2sqlem9  23849  2sqb  23854  pntrlog2bnd  23970  pntibndlem3  23978  pntlemp  23996  pnt3  23998  mirreu3  24239  axsegcon  24435  ax5seglem9  24445  axeuclid  24471  axcontlem12  24483  clwwlkf1  25001  wwlkext2clwwlk  25008  frgranbnb  25225  ablo4  25490  ghgrpOLD  25571  smcnlem  25808  pjhthmo  26421  pjpjpre  26538  3oalem2  26782  lnconi  27153  atom1d  27473  resf1o  27787  xrge0tsmsd  28013  ballotlemfc0  28698  ballotlemfcc  28699  pconcon  28943  cvmfolem  28991  cvmliftmo  28996  cvmliftlem7  29003  cvmlift2lem10  29024  cvmlift3lem8  29038  lineext  29957  linecgr  29962  btwnconn1lem10  29977  btwnconn1lem11  29978  btwnconn3  29984  brsegle  29989  seglecgr12im  29991  segleantisym  29996  outsideoftr  30010  outsideofeq  30011  outsideofeu  30012  linethru  30034  mblfinlem3  30296  bddiblnc  30328  ftc1cnnc  30332  finminlem  30379  neibastop2lem  30421  isbnd3  30523  heibor1lem  30548  crngm4  30643  mzpcl2  30905  mzpmfp  30922  mzpcompact2lem  30926  diophin  30948  pell14qrmulcl  31041  hbtlem2  31317  stoweidlem61  32085  fourierdlem92  32223  snlindsntor  33345  elfzolborelfzop1  33398  nn0sumshdiglemB  33514  cvlcvr1  35480  4atlem12  35752  paddasslem12  35971  paddasslem13  35972  lhpexle2lem  36149  trlord  36711  cdlemkid4  37076  dihopelvalcpre  37391  dihmeetlem1N  37433  dihglblem5apreN  37434  dihmeetlem6  37452  dih1dimatlem0  37471  dihjatcclem4  37564  iunrelexpuztr  38227
  Copyright terms: Public domain W3C validator