Theorem rexlimddv 3289

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2108  ∃wrex 3137

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1775  df-ral 3141  df-rex 3142

This theorem is referenced by:  oaabs2  8264  oemapvali  9139  cantnflem4  9147  r1pwss  9205  djuun  9347  infxpenc2lem1  9437  pwfseqlem3  10074  prlem934  10447  ltexprlem7  10456  reclem3pr  10463  00id  10807  mul02lem1  10808  addid2  10815  addcan  10816  addcan2  10817  negeu  10868  mulcand  11265  suprzcl  12054  uzwo3  12335  expmulnbnd  13588  limsupgre  14830  rlimclim1  14894  fsumcvg3  15078  oexpneg  15686  bitsfi  15778  vdwlem10  16318  mreexexlem4d  16910  mreexdomd  16912  isacs3lem  17768  grprinvlem  17875  grpridd  17877  grprcan  18129  sylow1  18720  pgpfi  18722  slwhash  18741  pj1id  18817  efgsfo  18857  efgredlemc  18863  dmdprdsplitlem  19151  dpjidcl  19172  pgpfac1lem4  19192  pgpfaclem2  19196  pgpfaclem3  19197  ablsimpgcygd  19220  ablsimpgfindlem1  19221  ablsimpgfind  19224  fincygsubgodexd  19227  ablsimpgprmd  19229  gsummgp0  19350  lspsolv  19907  restbas  21758  restcls  21781  restntr  21782  cnpnei  21864  cnpco  21867  pnrmopn  21943  1stcfb  22045  1stcrest  22053  2ndcctbss  22055  2ndcomap  22058  dis2ndc  22060  llyidm  22088  nllyidm  22089  hausllycmp  22094  lly1stc  22096  llycmpkgen2  22150  1stckgenlem  22153  basqtop  22311  regr1lem  22339  kqreglem1  22341  kqreglem2  22342  kqnrmlem1  22343  kqnrmlem2  22344  reghmph  22393  nrmhmph  22394  qtophmeo  22417  trfbas2  22443  fbasfip  22468  fbasrn  22484  trfg  22491  ssufl  22518  fmufil  22559  ufldom  22562  uffclsflim  22631  cnpfcfi  22640  alexsublem  22644  alexsubALTlem4  22650  ptcmplem3  22654  ptcmplem4  22655  tsmsxp  22755  met1stc  23123  met2ndci  23124  prdsxmslem2  23131  metcnpi3  23148  icccmplem1  23422  xrge0tsms  23434  metdseq0  23454  cnllycmp  23552  bndth  23554  lebnumlem1  23557  lebnum  23560  cfilfcls  23869  lmle  23896  relcmpcmet  23913  pjthlem2  24033  ovolscalem2  24107  ovolicc2lem4  24113  ovolicc2lem5  24114  ioombl1  24155  uniioombllem6  24181  uniioombl  24182  opnmbllem  24194  volivth  24200  mbfinf  24258  mbfi1fseqlem6  24313  itg2cnlem1  24354  itg2cn  24356  lhop2  24604  dvcnvre  24608  aareccl  24907  aaliou3lem8  24926  aaliou3lem9  24931  ulmdvlem3  24982  mtestbdd  24985  iblulm  24987  radcnvlem1  24993  abelthlem5  25015  abelthlem8  25019  chordthm  25407  dcubic  25416  lgambdd  25606  lgamucov  25607  lgamcvglem  25609  lgamcvg2  25624  fta  25649  dchrptlem2  25833  sumdchr2  25838  2sqlem11  25997  dchrisum  26060  dchrisum0flb  26078  pntibndlem3  26160  pntlemi  26172  pjspansn  29346  chscllem3  29408  xmulcand  30590  xrge0tsmsd  30685  esumpcvgval  31330  cnpconn  32470  pconnconn  32471  connpconn  32475  pconnpi1  32477  cnllysconn  32485  cvmcov2  32515  cvmliftpht  32558  mthmpps  32822  sinccvg  32909  btwnconn1lem13  33553  neibastop2lem  33701  tailfb  33718  unblimceq0lem  33838  knoppndvlem9  33852  knoppndvlem21  33864  knoppndvlem22  33865  matunitlindflem2  34881  poimirlem29  34913  opnmbllem0  34920  mblfinlem2  34922  mblfinlem4  34924  prdsbnd2  35065  cntotbnd  35066  heiborlem8  35088  heiborlem9  35089  cvlcvr1  36467  llnmlplnN  36667  cdlemb  36922  paddasslem10  36957  trlcnv  37293  trlator0  37299  trlid0  37304  trlnidatb  37305  cdlemd4  37329  cdlemg5  37733  trlco  37855  cdlemj3  37951  tendo0mul  37954  tendo0mulr  37955  tendoconid  37957  erngdv  38121  erngdv-rN  38129  dihmeetlem1N  38418  dihatlat  38462  hgmaprnlem5N  39028  remulcan2d  39147  renegeulemv  39189  remul02  39226  remul01  39228  remulinvcom  39239  remulid2  39240  remulcand  39241  prjspertr  39246  0prjspnrel  39260  acongrep  39568  jm2.27b  39594  lmhmfgsplit  39677  hbt  39721  imo72b2lem1  40512  mnuss2d  40591  mnuprdlem4  40602  mnuunid  40604  mnurndlem2  40609  cncmpmax  41280  rexlimddv2  42094  stoweidlem62  42338  oexpnegALTV  43833  oexpnegnz  43834  aacllem  44893