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

Theorem rexlimddv 3016
Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1 (𝜑 → ∃𝑥𝐴 𝜓)
rexlimddv.2 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
Assertion
Ref Expression
rexlimddv (𝜑𝜒)
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
2 rexlimddv.2 . . 3 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
32rexlimdvaa 3013 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  wcel 1976  wrex 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-ral 2900  df-rex 2901
This theorem is referenced by:  grprinvlem  6748  grpridd  6750  oaabs2  7590  oemapvali  8442  cantnflem4  8450  r1pwss  8508  infxpenc2lem1  8703  pwfseqlem3  9339  prlem934  9712  ltexprlem7  9721  reclem3pr  9728  00id  10063  mul02lem1  10064  addid2  10071  addcan  10072  addcan2  10073  negeu  10123  mulcand  10512  suprzcl  11292  uzwo3  11618  expmulnbnd  12816  limsupgre  14009  rlimclim1  14073  fsumcvg3  14256  oexpneg  14856  bitsfi  14946  vdwlem10  15481  mreexexlem4d  16079  mreexdomd  16082  isacs3lem  16938  grprcan  17227  sylow1  17790  pgpfi  17792  slwhash  17811  pj1id  17884  efgsfo  17924  efgredlemc  17930  dmdprdsplitlem  18208  dpjidcl  18229  pgpfac1lem4  18249  pgpfaclem2  18253  pgpfaclem3  18254  gsummgp0  18380  lspsolv  18913  restbas  20720  restcls  20743  restntr  20744  cnpnei  20826  cnpco  20829  pnrmopn  20905  1stcfb  21006  1stcrest  21014  2ndcctbss  21016  2ndcomap  21019  dis2ndc  21021  llyidm  21049  nllyidm  21050  hausllycmp  21055  lly1stc  21057  llycmpkgen2  21111  1stckgenlem  21114  basqtop  21272  regr1lem  21300  kqreglem1  21302  kqreglem2  21303  kqnrmlem1  21304  kqnrmlem2  21305  reghmph  21354  nrmhmph  21355  qtophmeo  21378  trfbas2  21405  fbasfip  21430  fbasrn  21446  trfg  21453  ssufl  21480  fmufil  21521  ufldom  21524  uffclsflim  21593  cnpfcfi  21602  alexsublem  21606  alexsubALTlem4  21612  ptcmplem3  21616  ptcmplem4  21617  tsmsxp  21716  met1stc  22084  met2ndci  22085  prdsxmslem2  22092  metcnpi3  22109  icccmplem1  22381  xrge0tsms  22393  metdseq0  22413  cnllycmp  22511  bndth  22513  lebnumlem1  22516  lebnum  22519  cfilfcls  22825  lmle  22852  relcmpcmet  22868  pjthlem2  22962  ovolscalem2  23034  ovolicc2lem4  23040  ovolicc2lem5  23041  ioombl1  23082  uniioombllem6  23107  uniioombl  23108  opnmbllem  23120  volivth  23126  mbfinf  23183  mbfi1fseqlem6  23238  itg2cnlem1  23279  itg2cn  23281  lhop2  23527  dvcnvre  23531  aareccl  23830  aaliou3lem8  23849  aaliou3lem9  23854  ulmdvlem3  23905  mtestbdd  23908  iblulm  23910  radcnvlem1  23916  abelthlem5  23938  abelthlem8  23942  chordthm  24309  dcubic  24318  lgambdd  24508  lgamucov  24509  lgamcvglem  24511  lgamcvg2  24526  fta  24551  dchrptlem2  24735  sumdchr2  24740  2sqlem11  24899  dchrisum  24926  dchrisum0flb  24944  pntibndlem3  25026  pntlemi  25038  pjspansn  27654  chscllem3  27716  xmulcand  28794  xrge0tsmsd  28950  esumpcvgval  29301  cnpcon  30300  pconcon  30301  conpcon  30305  pconpi1  30307  cnllyscon  30315  cvmcov2  30345  cvmliftpht  30388  mthmpps  30567  sinccvg  30655  btwnconn1lem13  31210  neibastop2lem  31359  tailfb  31376  unblimceq0lem  31501  knoppndvlem9  31515  knoppndvlem21  31527  knoppndvlem22  31528  matunitlindflem2  32400  poimirlem29  32432  opnmbllem0  32439  mblfinlem2  32441  mblfinlem4  32443  prdsbnd2  32588  cntotbnd  32589  heiborlem8  32611  heiborlem9  32612  cvlcvr1  33468  llnmlplnN  33667  cdlemb  33922  paddasslem10  33957  trlcnv  34294  trlator0  34300  trlid0  34305  trlnidatb  34306  cdlemd4  34330  cdlemg5  34735  trlco  34857  cdlemj3  34953  tendo0mul  34956  tendo0mulr  34957  tendoconid  34959  erngdv  35123  erngdv-rN  35131  dihmeetlem1N  35421  dihatlat  35465  hgmaprnlem5N  36034  acongrep  36389  jm2.27b  36415  lmhmfgsplit  36498  hbt  36543  imo72b2lem1  37317  cncmpmax  38038  stoweidlem62  38779  oexpnegALTV  39951  oexpnegnz  39952  aacllem  42339
  Copyright terms: Public domain W3C validator