Theorem rexlimddv 3017

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 3014	. 2 ⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝜓 → 𝜒))
4	1, 3	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977  ∃wrex 2897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-ral 2901  df-rex 2902

This theorem is referenced by:  grprinvlem  6770  grpridd  6772  oaabs2  7612  oemapvali  8464  cantnflem4  8472  r1pwss  8530  infxpenc2lem1  8725  pwfseqlem3  9361  prlem934  9734  ltexprlem7  9743  reclem3pr  9750  00id  10090  mul02lem1  10091  addid2  10098  addcan  10099  addcan2  10100  negeu  10150  mulcand  10539  suprzcl  11333  uzwo3  11659  expmulnbnd  12858  limsupgre  14060  rlimclim1  14124  fsumcvg3  14307  oexpneg  14907  bitsfi  14997  vdwlem10  15532  mreexexlem4d  16130  mreexdomd  16133  isacs3lem  16989  grprcan  17278  sylow1  17841  pgpfi  17843  slwhash  17862  pj1id  17935  efgsfo  17975  efgredlemc  17981  dmdprdsplitlem  18259  dpjidcl  18280  pgpfac1lem4  18300  pgpfaclem2  18304  pgpfaclem3  18305  gsummgp0  18431  lspsolv  18964  restbas  20772  restcls  20795  restntr  20796  cnpnei  20878  cnpco  20881  pnrmopn  20957  1stcfb  21058  1stcrest  21066  2ndcctbss  21068  2ndcomap  21071  dis2ndc  21073  llyidm  21101  nllyidm  21102  hausllycmp  21107  lly1stc  21109  llycmpkgen2  21163  1stckgenlem  21166  basqtop  21324  regr1lem  21352  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  reghmph  21406  nrmhmph  21407  qtophmeo  21430  trfbas2  21457  fbasfip  21482  fbasrn  21498  trfg  21505  ssufl  21532  fmufil  21573  ufldom  21576  uffclsflim  21645  cnpfcfi  21654  alexsublem  21658  alexsubALTlem4  21664  ptcmplem3  21668  ptcmplem4  21669  tsmsxp  21768  met1stc  22136  met2ndci  22137  prdsxmslem2  22144  metcnpi3  22161  icccmplem1  22433  xrge0tsms  22445  metdseq0  22465  cnllycmp  22563  bndth  22565  lebnumlem1  22568  lebnum  22571  cfilfcls  22880  lmle  22907  relcmpcmet  22923  pjthlem2  23017  ovolscalem2  23089  ovolicc2lem4  23095  ovolicc2lem5  23096  ioombl1  23137  uniioombllem6  23162  uniioombl  23163  opnmbllem  23175  volivth  23181  mbfinf  23238  mbfi1fseqlem6  23293  itg2cnlem1  23334  itg2cn  23336  lhop2  23582  dvcnvre  23586  aareccl  23885  aaliou3lem8  23904  aaliou3lem9  23909  ulmdvlem3  23960  mtestbdd  23963  iblulm  23965  radcnvlem1  23971  abelthlem5  23993  abelthlem8  23997  chordthm  24364  dcubic  24373  lgambdd  24563  lgamucov  24564  lgamcvglem  24566  lgamcvg2  24581  fta  24606  dchrptlem2  24790  sumdchr2  24795  2sqlem11  24954  dchrisum  24981  dchrisum0flb  24999  pntibndlem3  25081  pntlemi  25093  pjspansn  27820  chscllem3  27882  xmulcand  28960  xrge0tsmsd  29116  esumpcvgval  29467  cnpcon  30466  pconcon  30467  conpcon  30471  pconpi1  30473  cnllyscon  30481  cvmcov2  30511  cvmliftpht  30554  mthmpps  30733  sinccvg  30821  btwnconn1lem13  31376  neibastop2lem  31525  tailfb  31542  unblimceq0lem  31667  knoppndvlem9  31681  knoppndvlem21  31693  knoppndvlem22  31694  matunitlindflem2  32576  poimirlem29  32608  opnmbllem0  32615  mblfinlem2  32617  mblfinlem4  32619  prdsbnd2  32764  cntotbnd  32765  heiborlem8  32787  heiborlem9  32788  cvlcvr1  33644  llnmlplnN  33843  cdlemb  34098  paddasslem10  34133  trlcnv  34470  trlator0  34476  trlid0  34481  trlnidatb  34482  cdlemd4  34506  cdlemg5  34911  trlco  35033  cdlemj3  35129  tendo0mul  35132  tendo0mulr  35133  tendoconid  35135  erngdv  35299  erngdv-rN  35307  dihmeetlem1N  35597  dihatlat  35641  hgmaprnlem5N  36210  acongrep  36565  jm2.27b  36591  lmhmfgsplit  36674  hbt  36719  imo72b2lem1  37493  cncmpmax  38214  stoweidlem62  38955  oexpnegALTV  40126  oexpnegnz  40127  aacllem  42356