Theorem rexlimddv 3146

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119  ∃wrex 3063

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-rex 3064

This theorem is referenced by:  frxp2  8084  frxp3  8091  oaabs2  8575  oemapvali  9596  cantnflem4  9604  r1pwss  9699  djuun  9841  infxpenc2lem1  9932  pwfseqlem3  10574  prlem934  10947  ltexprlem7  10956  reclem3pr  10963  00id  11312  mul02lem1  11313  addlid  11320  addcan  11321  addcan2  11322  negeu  11374  mulcand  11774  suprzcl  12600  uzwo3  12884  expmulnbnd  14188  limsupgre  15434  rlimclim1  15498  fsumcvg3  15682  oexpneg  16305  bitsfi  16397  vdwlem10  16952  mreexexlem4d  17604  mreexdomd  17606  isacs3lem  18499  grpinvalem  18632  grprida  18634  grprcan  18940  sylow1  19569  pgpfi  19571  slwhash  19590  pj1id  19665  efgsfo  19705  efgredlemc  19711  dmdprdsplitlem  20005  dpjidcl  20026  pgpfac1lem4  20046  pgpfaclem2  20050  pgpfaclem3  20051  ablsimpgcygd  20074  ablsimpgfindlem1  20075  ablsimpgfind  20078  fincygsubgodexd  20081  ablsimpgprmd  20083  gsummgp0  20288  imadrhmcl  20769  lspsolv  21136  restbas  23141  restcls  23164  restntr  23165  cnpnei  23247  cnpco  23250  pnrmopn  23326  1stcfb  23428  1stcrest  23436  2ndcctbss  23438  2ndcomap  23441  dis2ndc  23443  llyidm  23471  nllyidm  23472  hausllycmp  23477  lly1stc  23479  llycmpkgen2  23533  1stckgenlem  23536  basqtop  23694  regr1lem  23722  kqreglem1  23724  kqreglem2  23725  kqnrmlem1  23726  kqnrmlem2  23727  reghmph  23776  nrmhmph  23777  qtophmeo  23800  trfbas2  23826  fbasfip  23851  fbasrn  23867  trfg  23874  ssufl  23901  fmufil  23942  ufldom  23945  uffclsflim  24014  cnpfcfi  24023  alexsublem  24027  alexsubALTlem4  24033  ptcmplem3  24037  ptcmplem4  24038  tsmsxp  24138  met1stc  24504  met2ndci  24505  prdsxmslem2  24512  metcnpi3  24529  icccmplem1  24806  xrge0tsms  24818  metdseq0  24838  cnllycmp  24941  bndth  24943  lebnumlem1  24946  lebnum  24949  cfilfcls  25259  lmle  25286  relcmpcmet  25303  pjthlem2  25423  ovolscalem2  25499  ovolicc2lem4  25505  ovolicc2lem5  25506  ioombl1  25547  uniioombllem6  25573  uniioombl  25574  opnmbllem  25586  volivth  25592  mbfinf  25650  mbfi1fseqlem6  25705  itg2cnlem1  25746  itg2cn  25748  lhop2  26000  dvcnvre  26004  aareccl  26310  aaliou3lem8  26329  aaliou3lem9  26334  ulmdvlem3  26385  mtestbdd  26388  iblulm  26390  radcnvlem1  26396  abelthlem5  26418  abelthlem8  26422  chordthm  26819  dcubic  26828  lgambdd  27018  lgamucov  27019  lgamcvglem  27021  lgamcvg2  27036  fta  27061  dchrptlem2  27246  sumdchr2  27251  2sqlem11  27410  dchrisum  27473  dchrisum0flb  27491  pntibndlem3  27573  pntlemi  27585  cutbdaybnd  27805  cofslts  27928  coinitslts  27929  addsproplem6  27984  negsproplem6  28043  mulsproplem13  28138  mulsproplem14  28139  recsne0  28202  recsex  28229  noseqp1  28301  pjspansn  31666  chscllem3  31728  xmulcand  32999  xrge0tsmsd  33154  esumpcvgval  34262  noinfepfnregs  35313  cnpconn  35458  pconnconn  35459  connpconn  35463  pconnpi1  35465  cnllysconn  35473  cvmcov2  35503  cvmliftpht  35546  mthmpps  35810  sinccvg  35901  btwnconn1lem13  36327  neibastop2lem  36588  tailfb  36605  weiunfr  36695  unblimceq0lem  36812  knoppndvlem9  36826  knoppndvlem21  36838  knoppndvlem22  36839  matunitlindflem2  37984  poimirlem29  38016  opnmbllem0  38023  mblfinlem2  38025  mblfinlem4  38027  prdsbnd2  38162  cntotbnd  38163  heiborlem8  38185  heiborlem9  38186  cvlcvr1  39831  llnmlplnN  40031  cdlemb  40286  paddasslem10  40321  trlcnv  40657  trlator0  40663  trlid0  40668  trlnidatb  40669  cdlemd4  40693  cdlemg5  41097  trlco  41219  cdlemj3  41315  tendo0mul  41318  tendo0mulr  41319  tendoconid  41321  erngdv  41485  erngdv-rN  41493  dihmeetlem1N  41782  dihatlat  41826  hgmaprnlem5N  42392  aks6d1c5  42624  remulcan2d  42740  renegeulemv  42845  remul02  42882  remul01  42884  sn-addcand  42897  sn-addrid  42898  sn-addcan2d  42899  sn-subeu  42904  remulinvcom  42910  remullid  42911  remulcand  42916  rediveud  42920  sn-0tie0  42941  imacrhmcl  43004  fiabv  43022  prjspertr  43055  0prjspnrel  43077  acongrep  43425  jm2.27b  43451  lmhmfgsplit  43531  hbt  43575  imo72b2lem1  44613  mnuss2d  44708  mnuprdlem4  44719  mnuunid  44721  mnurndlem2  44726  cncmpmax  45480  rexlimddv2  46266  stoweidlem62  46505  salrestss  46804  oexpnegALTV  48168  oexpnegnz  48169  upciclem4  49659  aacllem  50291