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

Theorem simprrl 741
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 444 . 2  |-  ( ( ch  /\  th )  ->  ch )
21ad2antll 710 1  |-  ( (
ph  /\  ( ps  /\  ( ch  /\  th ) ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  grpridd  6219  eroveu  6928  undom  7125  mapdom2  7207  domunfican  7308  fofinf1o  7316  finsschain  7341  wemaplem3  7443  oemapvali  7566  iunfictbso  7921  enfin2i  8127  fin1a2s  8220  ttukeylem6  8320  distrlem4pr  8829  divdivdiv  9640  divmuleq  9644  divsubdiv  9655  lediv12a  9828  xralrple  10716  seqcaopr  11280  leexp2r  11357  hashbclem  11621  rlimresb  12279  summo  12431  fsum2dlem  12474  bezoutlem3  12960  bezoutlem4  12961  qredeu  13027  pcqmul  13147  pcadd  13178  pockthg  13194  prmreclem2  13205  vdwlem10  13278  ramub1lem2  13315  mreexexlem4d  13792  mreexdomd  13794  issubc3  13966  cofucl  14005  setcmon  14162  setcepi  14163  drsdirfi  14315  poslubmo  14493  ghmpreima  14947  gaorber  15005  odcau  15158  pgpssslw  15168  fislw  15179  lsmsubm  15207  efgsfo  15291  gsum2d2  15468  pgpfac1lem5  15557  pgpfac1  15558  pgpfaclem2  15560  pgpfaclem3  15561  unitgrp  15692  lmodprop2d  15926  lsspropd  16013  lbsextlem4  16153  assapropd  16306  neiint  17084  restbas  17137  iscnp4  17242  cnpco  17246  nrmsep  17336  regsep2  17355  ordthauslem  17362  1stcfb  17422  1stcrest  17430  2ndcctbss  17432  2ndcdisj  17433  2ndcomap  17435  dis2ndc  17437  nlly2i  17453  islly2  17461  hausllycmp  17471  lly1stc  17473  ptbasin  17523  txcls  17550  ptcnp  17568  txlly  17582  txnlly  17583  txtube  17586  txcmplem1  17587  txcmplem2  17588  xkococnlem  17605  basqtop  17657  regr1lem  17685  kqreglem1  17687  kqreglem2  17688  kqnrmlem1  17689  kqnrmlem2  17690  reghmph  17739  nrmhmph  17740  opnfbas  17788  rnelfmlem  17898  fmufil  17905  fclscf  17971  fclsfnflim  17973  flimfnfcls  17974  uffclsflim  17977  cnpfcfi  17986  cnpfcf  17987  alexsubALTlem2  17993  alexsubALTlem4  17995  tgpconcompeqg  18055  ghmcnp  18058  divstgplem  18064  tsmsxp  18098  blss  18339  blcld  18418  metequiv2  18423  met2ndci  18435  prdsxmslem2  18442  txmetcnp  18460  nlmvscnlem1  18586  xrge0tsms  18729  ipcnlem1  19063  iscmet3  19110  cmetss  19131  minveclem3  19190  pmltpc  19207  ovolscalem2  19270  ovolicc2lem5  19277  ovolicc2  19278  nulmbl2  19291  ioombl1  19316  uniioombllem6  19340  uniioombl  19341  vitalilem3  19362  i1faddlem  19445  mbfmullem  19477  itg2split  19501  lhop2  19759  dvfsumrlim  19775  itgsubst  19793  evlslem1  19796  plydivex  20074  plyexmo  20090  ulmbdd  20174  cxploglim  20676  dchrptlem2  20909  lgsquad2lem2  21003  2sqlem5  21012  dchrvmasumif  21057  rpvmasum2  21066  dchrisum0re  21067  dchrisum0lem3  21073  dchrisum0  21074  dchrmusum  21078  dchrvmasum  21079  pntibndlem3  21146  pntlemp  21164  ostth3  21192  cusgrafilem1  21347  ablo4  21716  smcnlem  22034  pjhthmo  22645  mdslmd1lem1  23669  xrge0tsmsd  24045  xpinpreima2  24102  qqhval2  24158  dya2iocnrect  24418  orvcgteel  24497  orvclteel  24502  derangenlem  24629  cnpcon  24689  txpcon  24691  conpcon  24694  pconpi1  24696  iccllyscon  24709  rellyscon  24710  cvmcov2  24734  cvmliftmolem2  24741  cvmliftmo  24743  cvmliftlem15  24757  cvmliftpht  24777  cvmlift3lem2  24779  relexpsucl  24904  relexpcnv  24905  relexpdm  24907  relexprn  24908  relexpadd  24910  relexpindlem  24911  rtrclreclem.trans  24918  rtrclreclem.min  24919  rtrclind  24921  dedekind  24959  prodmo  25034  ax5seglem9  25583  ax5seg  25584  axcontlem8  25617  axcontlem12  25621  cgrextend  25649  btwnouttr2  25663  cgrsub  25686  cgrxfr  25696  btwnxfr  25697  colineardim1  25702  btwnconn1lem6  25733  btwnconn1lem13  25740  btwnconn1lem14  25741  btwnconn3  25744  seglecgr12im  25751  segleantisym  25756  outsideofeq  25771  outsidele  25773  lineunray  25788  linethru  25794  areacirclem6  25980  comppfsc  26071  neibastop2lem  26073  neibastop2  26074  istotbnd3  26164  sstotbnd  26168  crngm4  26297  diophin  26515  pellexlem3  26578  pellexlem5  26580  pellex  26582  pell14qrmulcl  26610  jm2.19lem3  26746  jm2.25  26754  jm2.27b  26761  lmhmfgsplit  26846  hbtlem2  26990  hbtlem5  26994  issubmd  27045  psgnunilem4  27082  psgneu  27091  fnchoice  27361  stoweidlem17  27427  stoweidlem53  27463  stoweidlem61  27471  cvlcvr1  29505  4atlem12  29777  paddasslem10  29994  paddasslem12  29996  paddasslem13  29997  lhpexle3lem  30176  cdlemd4  30366  cdleme0cq  30380  cdlemefs32sn1aw  30579  cdleme43fsv1snlem  30585  cdleme32d  30609  cdleme32f  30611  cdleme40m  30632  cdleme40n  30633  cdleme42keg  30651  cdleme42mgN  30653  cdleme50trn2  30716  cdleme50trn3  30718  cdlemm10N  31284  dihvalcqpre  31401  dihopelvalcpre  31414  dihmeetlem1N  31456  dihjat1lem  31594  mapd0  31831  mapdh9a  31956
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 178  df-an 361
  Copyright terms: Public domain W3C validator