Theorem rexlimddv 3136

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

Step	Hyp	Ref	Expression
1		rexlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥 ∈ 𝐴 𝜓)
2		rexlimddv.2	. . 3 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝜓)) → 𝜒)
3	2	rexlimdvaa 3131	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109  ∃wrex 3053

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3054

This theorem is referenced by:  frxp2  8084  frxp3  8091  oaabs2  8574  oemapvali  9599  cantnflem4  9607  r1pwss  9699  djuun  9841  infxpenc2lem1  9932  pwfseqlem3  10573  prlem934  10946  ltexprlem7  10955  reclem3pr  10962  00id  11309  mul02lem1  11310  addlid  11317  addcan  11318  addcan2  11319  negeu  11371  mulcand  11771  suprzcl  12574  uzwo3  12862  expmulnbnd  14160  limsupgre  15406  rlimclim1  15470  fsumcvg3  15654  oexpneg  16274  bitsfi  16366  vdwlem10  16920  mreexexlem4d  17571  mreexdomd  17573  isacs3lem  18466  grpinvalem  18565  grprida  18567  grprcan  18870  sylow1  19500  pgpfi  19502  slwhash  19521  pj1id  19596  efgsfo  19636  efgredlemc  19642  dmdprdsplitlem  19936  dpjidcl  19957  pgpfac1lem4  19977  pgpfaclem2  19981  pgpfaclem3  19982  ablsimpgcygd  20005  ablsimpgfindlem1  20006  ablsimpgfind  20009  fincygsubgodexd  20012  ablsimpgprmd  20014  gsummgp0  20221  imadrhmcl  20700  lspsolv  21068  restbas  23061  restcls  23084  restntr  23085  cnpnei  23167  cnpco  23170  pnrmopn  23246  1stcfb  23348  1stcrest  23356  2ndcctbss  23358  2ndcomap  23361  dis2ndc  23363  llyidm  23391  nllyidm  23392  hausllycmp  23397  lly1stc  23399  llycmpkgen2  23453  1stckgenlem  23456  basqtop  23614  regr1lem  23642  kqreglem1  23644  kqreglem2  23645  kqnrmlem1  23646  kqnrmlem2  23647  reghmph  23696  nrmhmph  23697  qtophmeo  23720  trfbas2  23746  fbasfip  23771  fbasrn  23787  trfg  23794  ssufl  23821  fmufil  23862  ufldom  23865  uffclsflim  23934  cnpfcfi  23943  alexsublem  23947  alexsubALTlem4  23953  ptcmplem3  23957  ptcmplem4  23958  tsmsxp  24058  met1stc  24425  met2ndci  24426  prdsxmslem2  24433  metcnpi3  24450  icccmplem1  24727  xrge0tsms  24739  metdseq0  24759  cnllycmp  24871  bndth  24873  lebnumlem1  24876  lebnum  24879  cfilfcls  25190  lmle  25217  relcmpcmet  25234  pjthlem2  25354  ovolscalem2  25431  ovolicc2lem4  25437  ovolicc2lem5  25438  ioombl1  25479  uniioombllem6  25505  uniioombl  25506  opnmbllem  25518  volivth  25524  mbfinf  25582  mbfi1fseqlem6  25637  itg2cnlem1  25678  itg2cn  25680  lhop2  25936  dvcnvre  25940  aareccl  26250  aaliou3lem8  26269  aaliou3lem9  26274  ulmdvlem3  26327  mtestbdd  26330  iblulm  26332  radcnvlem1  26338  abelthlem5  26361  abelthlem8  26365  chordthm  26763  dcubic  26772  lgambdd  26963  lgamucov  26964  lgamcvglem  26966  lgamcvg2  26981  fta  27006  dchrptlem2  27192  sumdchr2  27197  2sqlem11  27356  dchrisum  27419  dchrisum0flb  27437  pntibndlem3  27519  pntlemi  27531  scutbdaybnd  27744  cofsslt  27849  coinitsslt  27850  addsproplem6  27904  negsproplem6  27962  mulsproplem13  28054  mulsproplem14  28055  recsne0  28118  recsex  28144  noseqp1  28208  pjspansn  31539  chscllem3  31601  xmulcand  32874  xrge0tsmsd  33028  esumpcvgval  34047  cnpconn  35205  pconnconn  35206  connpconn  35210  pconnpi1  35212  cnllysconn  35220  cvmcov2  35250  cvmliftpht  35293  mthmpps  35557  sinccvg  35648  btwnconn1lem13  36075  neibastop2lem  36336  tailfb  36353  weiunfr  36443  unblimceq0lem  36482  knoppndvlem9  36496  knoppndvlem21  36508  knoppndvlem22  36509  matunitlindflem2  37599  poimirlem29  37631  opnmbllem0  37638  mblfinlem2  37640  mblfinlem4  37642  prdsbnd2  37777  cntotbnd  37778  heiborlem8  37800  heiborlem9  37801  cvlcvr1  39320  llnmlplnN  39521  cdlemb  39776  paddasslem10  39811  trlcnv  40147  trlator0  40153  trlid0  40158  trlnidatb  40159  cdlemd4  40183  cdlemg5  40587  trlco  40709  cdlemj3  40805  tendo0mul  40808  tendo0mulr  40809  tendoconid  40811  erngdv  40975  erngdv-rN  40983  dihmeetlem1N  41272  dihatlat  41316  hgmaprnlem5N  41882  aks6d1c5  42115  remulcan2d  42233  renegeulemv  42344  remul02  42381  remul01  42383  sn-addcand  42396  sn-addrid  42397  sn-addcan2d  42398  sn-subeu  42403  remulinvcom  42409  remullid  42410  remulcand  42415  rediveud  42419  sn-0tie0  42427  imacrhmcl  42490  fiabv  42512  prjspertr  42581  0prjspnrel  42603  acongrep  42956  jm2.27b  42982  lmhmfgsplit  43062  hbt  43106  imo72b2lem1  44145  mnuss2d  44240  mnuprdlem4  44251  mnuunid  44253  mnurndlem2  44258  cncmpmax  45013  rexlimddv2  45808  stoweidlem62  46047  salrestss  46346  oexpnegALTV  47665  oexpnegnz  47666  upciclem4  49158  aacllem  49790