Theorem rexlimddv 3137

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2110  ∃wrex 3054

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3055

This theorem is referenced by:  frxp2  8069  frxp3  8076  oaabs2  8559  oemapvali  9569  cantnflem4  9577  r1pwss  9669  djuun  9811  infxpenc2lem1  9902  pwfseqlem3  10543  prlem934  10916  ltexprlem7  10925  reclem3pr  10932  00id  11280  mul02lem1  11281  addlid  11288  addcan  11289  addcan2  11290  negeu  11342  mulcand  11742  suprzcl  12545  uzwo3  12833  expmulnbnd  14134  limsupgre  15380  rlimclim1  15444  fsumcvg3  15628  oexpneg  16248  bitsfi  16340  vdwlem10  16894  mreexexlem4d  17545  mreexdomd  17547  isacs3lem  18440  grpinvalem  18573  grprida  18575  grprcan  18878  sylow1  19508  pgpfi  19510  slwhash  19529  pj1id  19604  efgsfo  19644  efgredlemc  19650  dmdprdsplitlem  19944  dpjidcl  19965  pgpfac1lem4  19985  pgpfaclem2  19989  pgpfaclem3  19990  ablsimpgcygd  20013  ablsimpgfindlem1  20014  ablsimpgfind  20017  fincygsubgodexd  20020  ablsimpgprmd  20022  gsummgp0  20229  imadrhmcl  20705  lspsolv  21073  restbas  23066  restcls  23089  restntr  23090  cnpnei  23172  cnpco  23175  pnrmopn  23251  1stcfb  23353  1stcrest  23361  2ndcctbss  23363  2ndcomap  23366  dis2ndc  23368  llyidm  23396  nllyidm  23397  hausllycmp  23402  lly1stc  23404  llycmpkgen2  23458  1stckgenlem  23461  basqtop  23619  regr1lem  23647  kqreglem1  23649  kqreglem2  23650  kqnrmlem1  23651  kqnrmlem2  23652  reghmph  23701  nrmhmph  23702  qtophmeo  23725  trfbas2  23751  fbasfip  23776  fbasrn  23792  trfg  23799  ssufl  23826  fmufil  23867  ufldom  23870  uffclsflim  23939  cnpfcfi  23948  alexsublem  23952  alexsubALTlem4  23958  ptcmplem3  23962  ptcmplem4  23963  tsmsxp  24063  met1stc  24429  met2ndci  24430  prdsxmslem2  24437  metcnpi3  24454  icccmplem1  24731  xrge0tsms  24743  metdseq0  24763  cnllycmp  24875  bndth  24877  lebnumlem1  24880  lebnum  24883  cfilfcls  25194  lmle  25221  relcmpcmet  25238  pjthlem2  25358  ovolscalem2  25435  ovolicc2lem4  25441  ovolicc2lem5  25442  ioombl1  25483  uniioombllem6  25509  uniioombl  25510  opnmbllem  25522  volivth  25528  mbfinf  25586  mbfi1fseqlem6  25641  itg2cnlem1  25682  itg2cn  25684  lhop2  25940  dvcnvre  25944  aareccl  26254  aaliou3lem8  26273  aaliou3lem9  26278  ulmdvlem3  26331  mtestbdd  26334  iblulm  26336  radcnvlem1  26342  abelthlem5  26365  abelthlem8  26369  chordthm  26767  dcubic  26776  lgambdd  26967  lgamucov  26968  lgamcvglem  26970  lgamcvg2  26985  fta  27010  dchrptlem2  27196  sumdchr2  27201  2sqlem11  27360  dchrisum  27423  dchrisum0flb  27441  pntibndlem3  27523  pntlemi  27535  scutbdaybnd  27749  cofsslt  27855  coinitsslt  27856  addsproplem6  27910  negsproplem6  27968  mulsproplem13  28060  mulsproplem14  28061  recsne0  28124  recsex  28150  noseqp1  28214  pjspansn  31547  chscllem3  31609  xmulcand  32891  xrge0tsmsd  33032  esumpcvgval  34081  cnpconn  35242  pconnconn  35243  connpconn  35247  pconnpi1  35249  cnllysconn  35257  cvmcov2  35287  cvmliftpht  35330  mthmpps  35594  sinccvg  35685  btwnconn1lem13  36112  neibastop2lem  36373  tailfb  36390  weiunfr  36480  unblimceq0lem  36519  knoppndvlem9  36533  knoppndvlem21  36545  knoppndvlem22  36546  matunitlindflem2  37636  poimirlem29  37668  opnmbllem0  37675  mblfinlem2  37677  mblfinlem4  37679  prdsbnd2  37814  cntotbnd  37815  heiborlem8  37837  heiborlem9  37838  cvlcvr1  39357  llnmlplnN  39557  cdlemb  39812  paddasslem10  39847  trlcnv  40183  trlator0  40189  trlid0  40194  trlnidatb  40195  cdlemd4  40219  cdlemg5  40623  trlco  40745  cdlemj3  40841  tendo0mul  40844  tendo0mulr  40845  tendoconid  40847  erngdv  41011  erngdv-rN  41019  dihmeetlem1N  41308  dihatlat  41352  hgmaprnlem5N  41918  aks6d1c5  42151  remulcan2d  42269  renegeulemv  42380  remul02  42417  remul01  42419  sn-addcand  42432  sn-addrid  42433  sn-addcan2d  42434  sn-subeu  42439  remulinvcom  42445  remullid  42446  remulcand  42451  rediveud  42455  sn-0tie0  42463  imacrhmcl  42526  fiabv  42548  prjspertr  42617  0prjspnrel  42639  acongrep  42992  jm2.27b  43018  lmhmfgsplit  43098  hbt  43142  imo72b2lem1  44181  mnuss2d  44276  mnuprdlem4  44287  mnuunid  44289  mnurndlem2  44294  cncmpmax  45048  rexlimddv2  45840  stoweidlem62  46079  salrestss  46378  oexpnegALTV  47687  oexpnegnz  47688  upciclem4  49180  aacllem  49812