Theorem rexlimddv 3203

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110  ∃wrex 3055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-ral 3059  df-rex 3060

This theorem is referenced by:  oaabs2  8363  oemapvali  9288  cantnflem4  9296  r1pwss  9383  djuun  9525  infxpenc2lem1  9616  pwfseqlem3  10257  prlem934  10630  ltexprlem7  10639  reclem3pr  10646  00id  10990  mul02lem1  10991  addid2  10998  addcan  10999  addcan2  11000  negeu  11051  mulcand  11448  suprzcl  12240  uzwo3  12522  expmulnbnd  13785  limsupgre  15025  rlimclim1  15089  fsumcvg3  15276  oexpneg  15887  bitsfi  15977  vdwlem10  16524  mreexexlem4d  17122  mreexdomd  17124  isacs3lem  18020  grprinvlem  18117  grpridd  18119  grprcan  18373  sylow1  18964  pgpfi  18966  slwhash  18985  pj1id  19061  efgsfo  19101  efgredlemc  19107  dmdprdsplitlem  19396  dpjidcl  19417  pgpfac1lem4  19437  pgpfaclem2  19441  pgpfaclem3  19442  ablsimpgcygd  19465  ablsimpgfindlem1  19466  ablsimpgfind  19469  fincygsubgodexd  19472  ablsimpgprmd  19474  gsummgp0  19598  lspsolv  20152  restbas  22027  restcls  22050  restntr  22051  cnpnei  22133  cnpco  22136  pnrmopn  22212  1stcfb  22314  1stcrest  22322  2ndcctbss  22324  2ndcomap  22327  dis2ndc  22329  llyidm  22357  nllyidm  22358  hausllycmp  22363  lly1stc  22365  llycmpkgen2  22419  1stckgenlem  22422  basqtop  22580  regr1lem  22608  kqreglem1  22610  kqreglem2  22611  kqnrmlem1  22612  kqnrmlem2  22613  reghmph  22662  nrmhmph  22663  qtophmeo  22686  trfbas2  22712  fbasfip  22737  fbasrn  22753  trfg  22760  ssufl  22787  fmufil  22828  ufldom  22831  uffclsflim  22900  cnpfcfi  22909  alexsublem  22913  alexsubALTlem4  22919  ptcmplem3  22923  ptcmplem4  22924  tsmsxp  23024  met1stc  23391  met2ndci  23392  prdsxmslem2  23399  metcnpi3  23416  icccmplem1  23691  xrge0tsms  23703  metdseq0  23723  cnllycmp  23825  bndth  23827  lebnumlem1  23830  lebnum  23833  cfilfcls  24143  lmle  24170  relcmpcmet  24187  pjthlem2  24307  ovolscalem2  24383  ovolicc2lem4  24389  ovolicc2lem5  24390  ioombl1  24431  uniioombllem6  24457  uniioombl  24458  opnmbllem  24470  volivth  24476  mbfinf  24534  mbfi1fseqlem6  24590  itg2cnlem1  24631  itg2cn  24633  lhop2  24884  dvcnvre  24888  aareccl  25191  aaliou3lem8  25210  aaliou3lem9  25215  ulmdvlem3  25266  mtestbdd  25269  iblulm  25271  radcnvlem1  25277  abelthlem5  25299  abelthlem8  25303  chordthm  25692  dcubic  25701  lgambdd  25891  lgamucov  25892  lgamcvglem  25894  lgamcvg2  25909  fta  25934  dchrptlem2  26118  sumdchr2  26123  2sqlem11  26282  dchrisum  26345  dchrisum0flb  26363  pntibndlem3  26445  pntlemi  26457  pjspansn  29630  chscllem3  29692  xmulcand  30887  xrge0tsmsd  31008  esumpcvgval  31730  cnpconn  32877  pconnconn  32878  connpconn  32882  pconnpi1  32884  cnllysconn  32892  cvmcov2  32922  cvmliftpht  32965  mthmpps  33229  sinccvg  33316  frxp2  33479  frxp3  33485  scutbdaybnd  33703  cofsslt  33782  coinitsslt  33783  btwnconn1lem13  34095  neibastop2lem  34243  tailfb  34260  unblimceq0lem  34380  knoppndvlem9  34394  knoppndvlem21  34406  knoppndvlem22  34407  matunitlindflem2  35468  poimirlem29  35500  opnmbllem0  35507  mblfinlem2  35509  mblfinlem4  35511  prdsbnd2  35647  cntotbnd  35648  heiborlem8  35670  heiborlem9  35671  cvlcvr1  37047  llnmlplnN  37247  cdlemb  37502  paddasslem10  37537  trlcnv  37873  trlator0  37879  trlid0  37884  trlnidatb  37885  cdlemd4  37909  cdlemg5  38313  trlco  38435  cdlemj3  38531  tendo0mul  38534  tendo0mulr  38535  tendoconid  38537  erngdv  38701  erngdv-rN  38709  dihmeetlem1N  38998  dihatlat  39042  hgmaprnlem5N  39608  remulcan2d  39952  renegeulemv  40011  remul02  40048  remul01  40050  sn-addcand  40061  sn-addid1  40062  sn-addcan2d  40063  sn-subeu  40068  remulinvcom  40074  remulid2  40075  remulcand  40080  sn-0tie0  40081  itrere  40096  retire  40097  prjspertr  40104  0prjspnrel  40124  acongrep  40457  jm2.27b  40483  lmhmfgsplit  40566  hbt  40610  imo72b2lem1  41409  mnuss2d  41507  mnuprdlem4  41518  mnuunid  41520  mnurndlem2  41525  cncmpmax  42200  rexlimddv2  42993  stoweidlem62  43232  oexpnegALTV  44756  oexpnegnz  44757  aacllem  46130