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

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

Proof of Theorem simprrl
StepHypRef Expression
1 simpl 454 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 723 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
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:  grpridd  6294  eroveu  7185  undom  7389  mapdom2  7472  domunfican  7574  fofinf1o  7582  finsschain  7608  wemaplem3  7752  oemapvali  7882  iunfictbso  8274  enfin2i  8480  fin1a2s  8573  ttukeylem6  8673  distrlem4pr  9185  dedekind  9523  divdivdiv  10022  divmuleq  10026  divsubdiv  10037  lediv12a  10215  xralrple  11165  ssfzo12bi  11608  seqcaopr  11829  leexp2r  11907  hashbclem  12191  wrd2ind  12358  rlimresb  13029  summo  13180  fsum2dlem  13223  bezoutlem3  13709  bezoutlem4  13710  qredeu  13778  pcqmul  13905  pcadd  13936  pockthg  13952  prmreclem2  13963  vdwlem10  14036  ramub1lem2  14073  cshwsdisj  14110  mreexexlem4d  14570  mreexdomd  14572  issubc3  14744  cofucl  14783  setcmon  14940  setcepi  14941  drsdirfi  15093  poslubmo  15301  posglbmo  15302  issubmd  15461  mrcmndind  15478  ghmpreima  15750  gaorber  15808  psgnunilem4  15985  psgneu  15994  odcau  16085  pgpssslw  16095  fislw  16106  lsmsubm  16134  efgsfo  16218  gsum2d2  16442  pgpfac1lem5  16556  pgpfac1  16557  pgpfaclem2  16559  pgpfaclem3  16560  unitgrp  16695  lmodprop2d  16933  lsspropd  17022  lbsextlem4  17166  assapropd  17322  mdetunilem8  18269  mdetuni0  18271  mdetmul  18273  neiint  18552  restbas  18606  iscnp4  18711  cnpco  18715  nrmsep  18805  regsep2  18824  ordthauslem  18831  1stcfb  18893  1stcrest  18901  2ndcctbss  18903  2ndcdisj  18904  2ndcomap  18906  dis2ndc  18908  nlly2i  18924  islly2  18932  hausllycmp  18942  lly1stc  18944  ptbasin  18994  txcls  19021  ptcnp  19039  txlly  19053  txnlly  19054  txtube  19057  txcmplem1  19058  txcmplem2  19059  xkococnlem  19076  basqtop  19128  regr1lem  19156  kqreglem1  19158  kqreglem2  19159  kqnrmlem1  19160  kqnrmlem2  19161  reghmph  19210  nrmhmph  19211  opnfbas  19259  rnelfmlem  19369  fmufil  19376  fclscf  19442  fclsfnflim  19444  flimfnfcls  19445  uffclsflim  19448  cnpfcfi  19457  cnpfcf  19458  alexsubALTlem2  19464  alexsubALTlem4  19466  tgpconcompeqg  19526  ghmcnp  19529  divstgplem  19535  tsmsxp  19573  blssps  19843  blss  19844  blcld  19924  metequiv2  19929  met2ndci  19941  prdsxmslem2  19948  txmetcnp  19966  nlmvscnlem1  20111  xrge0tsms  20255  ipcnlem1  20601  iscmet3  20648  cmetss  20669  minveclem3  20760  pmltpc  20778  ovolscalem2  20841  ovolicc2lem5  20848  ovolicc2  20849  nulmbl2  20862  ioombl1  20887  uniioombllem6  20912  uniioombl  20913  vitalilem3  20934  i1faddlem  21015  mbfmullem  21047  itg2split  21071  lhop2  21331  dvfsumrlim  21347  itgsubst  21365  evlslem1  21369  plydivex  21650  plyexmo  21666  ulmbdd  21750  cxploglim  22258  dchrptlem2  22491  lgsquad2lem2  22585  2sqlem5  22594  dchrvmasumif  22639  rpvmasum2  22648  dchrisum0re  22649  dchrisum0lem3  22655  dchrisum0  22656  dchrmusum  22660  dchrvmasum  22661  pntibndlem3  22728  pntlemp  22746  ostth3  22774  legtrid  22900  mirreu3  22926  ax5seglem9  23008  ax5seg  23009  axcontlem8  23042  axcontlem12  23046  cusgrafilem1  23212  ablo4  23599  smcnlem  23917  pjhthmo  24530  mdslmd1lem1  25554  xrge0tsmsd  26108  xpinpreima2  26193  qqhval2  26267  dya2iocnrect  26552  orvcgteel  26700  orvclteel  26705  derangenlem  26909  cnpcon  26969  txpcon  26971  conpcon  26974  pconpi1  26976  iccllyscon  26989  rellyscon  26990  cvmcov2  27014  cvmliftmolem2  27021  cvmliftmo  27023  cvmliftlem15  27037  cvmliftpht  27057  cvmlift3lem2  27059  relexpsucl  27183  relexpcnv  27184  relexpdm  27186  relexprn  27187  relexpadd  27189  relexpindlem  27190  rtrclreclem.trans  27197  rtrclreclem.min  27198  rtrclind  27200  prodmo  27298  fprod2dlem  27340  cgrextend  27888  btwnouttr2  27902  cgrsub  27925  cgrxfr  27935  btwnxfr  27936  colineardim1  27941  btwnconn1lem6  27972  btwnconn1lem13  27979  btwnconn1lem14  27980  btwnconn3  27983  seglecgr12im  27990  segleantisym  27995  outsideofeq  28010  outsidele  28012  lineunray  28027  linethru  28033  mblfinlem3  28276  cnambfre  28286  areacirclem5  28334  comppfsc  28425  neibastop2lem  28427  neibastop2  28428  istotbnd3  28516  sstotbnd  28520  crngm4  28649  diophin  28958  pellexlem3  29019  pellexlem5  29021  pellex  29023  pell14qrmulcl  29051  jm2.19lem3  29187  jm2.25  29195  jm2.27b  29202  lmhmfgsplit  29286  hbtlem2  29327  hbtlem5  29331  fnchoice  29598  stoweidlem17  29660  stoweidlem53  29696  stoweidlem61  29704  2spotiundisj  30503  lindslinindsimp1  30740  bj-finsumval0  32199  cvlcvr1  32597  4atlem12  32869  paddasslem10  33086  paddasslem12  33088  paddasslem13  33089  lhpexle3lem  33268  cdlemd4  33458  cdleme0cq  33472  cdlemefs32sn1aw  33671  cdleme43fsv1snlem  33677  cdleme32d  33701  cdleme32f  33703  cdleme40m  33724  cdleme40n  33725  cdleme42keg  33743  cdleme42mgN  33745  cdleme50trn2  33808  cdleme50trn3  33810  cdlemm10N  34376  dihvalcqpre  34493  dihopelvalcpre  34506  dihmeetlem1N  34548  dihjat1lem  34686  mapd0  34923  mapdh9a  35048
  Copyright terms: Public domain W3C validator