Theorem rexlimddv 3219

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-ral 3068  df-rex 3069

This theorem is referenced by:  oaabs2  8439  oemapvali  9372  cantnflem4  9380  r1pwss  9473  djuun  9615  infxpenc2lem1  9706  pwfseqlem3  10347  prlem934  10720  ltexprlem7  10729  reclem3pr  10736  00id  11080  mul02lem1  11081  addid2  11088  addcan  11089  addcan2  11090  negeu  11141  mulcand  11538  suprzcl  12330  uzwo3  12612  expmulnbnd  13878  limsupgre  15118  rlimclim1  15182  fsumcvg3  15369  oexpneg  15982  bitsfi  16072  vdwlem10  16619  mreexexlem4d  17273  mreexdomd  17275  isacs3lem  18175  grprinvlem  18272  grpridd  18274  grprcan  18528  sylow1  19123  pgpfi  19125  slwhash  19144  pj1id  19220  efgsfo  19260  efgredlemc  19266  dmdprdsplitlem  19555  dpjidcl  19576  pgpfac1lem4  19596  pgpfaclem2  19600  pgpfaclem3  19601  ablsimpgcygd  19624  ablsimpgfindlem1  19625  ablsimpgfind  19628  fincygsubgodexd  19631  ablsimpgprmd  19633  gsummgp0  19762  lspsolv  20320  restbas  22217  restcls  22240  restntr  22241  cnpnei  22323  cnpco  22326  pnrmopn  22402  1stcfb  22504  1stcrest  22512  2ndcctbss  22514  2ndcomap  22517  dis2ndc  22519  llyidm  22547  nllyidm  22548  hausllycmp  22553  lly1stc  22555  llycmpkgen2  22609  1stckgenlem  22612  basqtop  22770  regr1lem  22798  kqreglem1  22800  kqreglem2  22801  kqnrmlem1  22802  kqnrmlem2  22803  reghmph  22852  nrmhmph  22853  qtophmeo  22876  trfbas2  22902  fbasfip  22927  fbasrn  22943  trfg  22950  ssufl  22977  fmufil  23018  ufldom  23021  uffclsflim  23090  cnpfcfi  23099  alexsublem  23103  alexsubALTlem4  23109  ptcmplem3  23113  ptcmplem4  23114  tsmsxp  23214  met1stc  23583  met2ndci  23584  prdsxmslem2  23591  metcnpi3  23608  icccmplem1  23891  xrge0tsms  23903  metdseq0  23923  cnllycmp  24025  bndth  24027  lebnumlem1  24030  lebnum  24033  cfilfcls  24343  lmle  24370  relcmpcmet  24387  pjthlem2  24507  ovolscalem2  24583  ovolicc2lem4  24589  ovolicc2lem5  24590  ioombl1  24631  uniioombllem6  24657  uniioombl  24658  opnmbllem  24670  volivth  24676  mbfinf  24734  mbfi1fseqlem6  24790  itg2cnlem1  24831  itg2cn  24833  lhop2  25084  dvcnvre  25088  aareccl  25391  aaliou3lem8  25410  aaliou3lem9  25415  ulmdvlem3  25466  mtestbdd  25469  iblulm  25471  radcnvlem1  25477  abelthlem5  25499  abelthlem8  25503  chordthm  25892  dcubic  25901  lgambdd  26091  lgamucov  26092  lgamcvglem  26094  lgamcvg2  26109  fta  26134  dchrptlem2  26318  sumdchr2  26323  2sqlem11  26482  dchrisum  26545  dchrisum0flb  26563  pntibndlem3  26645  pntlemi  26657  pjspansn  29840  chscllem3  29902  xmulcand  31097  xrge0tsmsd  31219  esumpcvgval  31946  cnpconn  33092  pconnconn  33093  connpconn  33097  pconnpi1  33099  cnllysconn  33107  cvmcov2  33137  cvmliftpht  33180  mthmpps  33444  sinccvg  33531  frxp2  33718  frxp3  33724  scutbdaybnd  33936  cofsslt  34015  coinitsslt  34016  btwnconn1lem13  34328  neibastop2lem  34476  tailfb  34493  unblimceq0lem  34613  knoppndvlem9  34627  knoppndvlem21  34639  knoppndvlem22  34640  matunitlindflem2  35701  poimirlem29  35733  opnmbllem0  35740  mblfinlem2  35742  mblfinlem4  35744  prdsbnd2  35880  cntotbnd  35881  heiborlem8  35903  heiborlem9  35904  cvlcvr1  37280  llnmlplnN  37480  cdlemb  37735  paddasslem10  37770  trlcnv  38106  trlator0  38112  trlid0  38117  trlnidatb  38118  cdlemd4  38142  cdlemg5  38546  trlco  38668  cdlemj3  38764  tendo0mul  38767  tendo0mulr  38768  tendoconid  38770  erngdv  38934  erngdv-rN  38942  dihmeetlem1N  39231  dihatlat  39275  hgmaprnlem5N  39841  remulcan2d  40214  renegeulemv  40272  remul02  40309  remul01  40311  sn-addcand  40322  sn-addid1  40323  sn-addcan2d  40324  sn-subeu  40329  remulinvcom  40335  remulid2  40336  remulcand  40341  sn-0tie0  40342  itrere  40357  retire  40358  prjspertr  40365  0prjspnrel  40385  acongrep  40718  jm2.27b  40744  lmhmfgsplit  40827  hbt  40871  imo72b2lem1  41669  mnuss2d  41771  mnuprdlem4  41782  mnuunid  41784  mnurndlem2  41789  cncmpmax  42464  rexlimddv2  43254  stoweidlem62  43493  oexpnegALTV  45017  oexpnegnz  45018  aacllem  46391