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

Theorem rexlimddv 2840
Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1  |-  ( ph  ->  E. x  e.  A  ps )
rexlimddv.2  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
Assertion
Ref Expression
rexlimddv  |-  ( ph  ->  ch )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2  |-  ( ph  ->  E. x  e.  A  ps )
2 rexlimddv.2 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
32rexlimdvaa 2837 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
41, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    e. wcel 1756   E.wrex 2711
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-12 1792
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-ral 2715  df-rex 2716
This theorem is referenced by:  grprinvlem  6296  grpridd  6298  oaabs2  7076  oemapvali  7884  cantnflem4  7892  cantnflem4OLD  7914  r1pwss  7983  infxpenc2lem1  8177  pwfseqlem3  8819  prlem934  9194  ltexprlem7  9203  reclem3pr  9210  00id  9536  mul02lem1  9537  addid2  9544  addcan  9545  addcan2  9546  negeu  9592  mulcand  9961  suprzcl  10713  uzwo3  10940  expmulnbnd  11988  limsupgre  12951  rlimclim1  13015  fsumcvg3  13198  oexpneg  13587  bitsfi  13625  vdwlem10  14043  mreexexlem4d  14577  mreexdomd  14579  isacs3lem  15328  grprcan  15562  sylow1  16093  pgpfi  16095  slwhash  16114  pj1id  16187  efgsfo  16227  efgredlemc  16233  dmdprdsplitlem  16522  dmdprdsplitlemOLD  16523  dpjidcl  16545  dpjidclOLD  16552  pgpfac1lem4  16567  pgpfaclem2  16571  pgpfaclem3  16572  gsummgp0  16687  lspsolv  17201  restbas  18737  restcls  18760  restntr  18761  cnpnei  18843  cnpco  18846  pnrmopn  18922  1stcfb  19024  1stcrest  19032  2ndcctbss  19034  2ndcomap  19037  dis2ndc  19039  llyidm  19067  nllyidm  19068  hausllycmp  19073  lly1stc  19075  llycmpkgen2  19098  1stckgenlem  19101  basqtop  19259  regr1lem  19287  kqreglem1  19289  kqreglem2  19290  kqnrmlem1  19291  kqnrmlem2  19292  reghmph  19341  nrmhmph  19342  qtophmeo  19365  trfbas2  19391  fbasfip  19416  fbasrn  19432  trfg  19439  ssufl  19466  fmufil  19507  ufldom  19510  uffclsflim  19579  cnpfcfi  19588  alexsublem  19591  alexsubALTlem4  19597  ptcmplem3  19601  ptcmplem4  19602  tsmsxp  19704  met1stc  20071  met2ndci  20072  prdsxmslem2  20079  metcnpi3  20096  icccmplem1  20374  xrge0tsms  20386  metdseq0  20405  cnllycmp  20503  bndth  20505  lebnumlem1  20508  lebnum  20511  cfilfcls  20760  lmle  20787  relcmpcmet  20802  pjthlem2  20900  ovolscalem2  20972  ovolicc2lem4  20978  ovolicc2lem5  20979  ioombl1  21018  uniioombllem6  21043  uniioombl  21044  opnmbllem  21056  volivth  21062  mbfinf  21118  mbfi1fseqlem6  21173  itg2cnlem1  21214  itg2cn  21216  lhop2  21462  dvcnvre  21466  aareccl  21767  aaliou3lem8  21786  aaliou3lem9  21791  ulmdvlem3  21842  mtestbdd  21845  iblulm  21847  radcnvlem1  21853  abelthlem5  21875  abelthlem8  21879  chordthm  22207  dcubic  22216  fta  22392  dchrptlem2  22579  sumdchr2  22584  2sqlem11  22689  dchrisum  22716  dchrisum0flb  22734  pntibndlem3  22816  pntlemi  22828  pjspansn  24931  chscllem3  24993  xmulcand  26047  xrge0tsmsd  26204  esumpcvgval  26479  lgambdd  26975  lgamucov  26976  lgamcvglem  26978  lgamcvg2  26993  cnpcon  27071  pconcon  27072  conpcon  27076  pconpi1  27078  cnllyscon  27086  cvmcov2  27116  cvmliftpht  27159  sinccvg  27269  btwnconn1lem13  28081  opnmbllem0  28380  mblfinlem2  28382  mblfinlem4  28384  neibastop2lem  28534  tailfb  28551  prdsbnd2  28647  cntotbnd  28648  heiborlem8  28670  heiborlem9  28671  acongrep  29276  jm2.27b  29308  lmhmfgsplit  29392  hbt  29439  cncmpmax  29707  stoweidlem62  29810  cvlcvr1  32824  llnmlplnN  33023  cdlemb  33278  paddasslem10  33313  trlcnv  33649  trlator0  33655  trlid0  33660  trlnidatb  33661  cdlemd4  33685  cdlemg5  34089  trlco  34211  cdlemj3  34307  tendo0mul  34310  tendo0mulr  34311  tendoconid  34313  erngdv  34477  erngdv-rN  34485  dihmeetlem1N  34775  dihatlat  34819  hgmaprnlem5N  35388
  Copyright terms: Public domain W3C validator