Theorem rexlimddv 3139

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111  ∃wrex 3056

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 3057

This theorem is referenced by:  frxp2  8074  frxp3  8081  oaabs2  8564  oemapvali  9574  cantnflem4  9582  r1pwss  9677  djuun  9819  infxpenc2lem1  9910  pwfseqlem3  10551  prlem934  10924  ltexprlem7  10933  reclem3pr  10940  00id  11288  mul02lem1  11289  addlid  11296  addcan  11297  addcan2  11298  negeu  11350  mulcand  11750  suprzcl  12553  uzwo3  12841  expmulnbnd  14142  limsupgre  15388  rlimclim1  15452  fsumcvg3  15636  oexpneg  16256  bitsfi  16348  vdwlem10  16902  mreexexlem4d  17553  mreexdomd  17555  isacs3lem  18448  grpinvalem  18581  grprida  18583  grprcan  18886  sylow1  19516  pgpfi  19518  slwhash  19537  pj1id  19612  efgsfo  19652  efgredlemc  19658  dmdprdsplitlem  19952  dpjidcl  19973  pgpfac1lem4  19993  pgpfaclem2  19997  pgpfaclem3  19998  ablsimpgcygd  20021  ablsimpgfindlem1  20022  ablsimpgfind  20025  fincygsubgodexd  20028  ablsimpgprmd  20030  gsummgp0  20237  imadrhmcl  20713  lspsolv  21081  restbas  23074  restcls  23097  restntr  23098  cnpnei  23180  cnpco  23183  pnrmopn  23259  1stcfb  23361  1stcrest  23369  2ndcctbss  23371  2ndcomap  23374  dis2ndc  23376  llyidm  23404  nllyidm  23405  hausllycmp  23410  lly1stc  23412  llycmpkgen2  23466  1stckgenlem  23469  basqtop  23627  regr1lem  23655  kqreglem1  23657  kqreglem2  23658  kqnrmlem1  23659  kqnrmlem2  23660  reghmph  23709  nrmhmph  23710  qtophmeo  23733  trfbas2  23759  fbasfip  23784  fbasrn  23800  trfg  23807  ssufl  23834  fmufil  23875  ufldom  23878  uffclsflim  23947  cnpfcfi  23956  alexsublem  23960  alexsubALTlem4  23966  ptcmplem3  23970  ptcmplem4  23971  tsmsxp  24071  met1stc  24437  met2ndci  24438  prdsxmslem2  24445  metcnpi3  24462  icccmplem1  24739  xrge0tsms  24751  metdseq0  24771  cnllycmp  24883  bndth  24885  lebnumlem1  24888  lebnum  24891  cfilfcls  25202  lmle  25229  relcmpcmet  25246  pjthlem2  25366  ovolscalem2  25443  ovolicc2lem4  25449  ovolicc2lem5  25450  ioombl1  25491  uniioombllem6  25517  uniioombl  25518  opnmbllem  25530  volivth  25536  mbfinf  25594  mbfi1fseqlem6  25649  itg2cnlem1  25690  itg2cn  25692  lhop2  25948  dvcnvre  25952  aareccl  26262  aaliou3lem8  26281  aaliou3lem9  26286  ulmdvlem3  26339  mtestbdd  26342  iblulm  26344  radcnvlem1  26350  abelthlem5  26373  abelthlem8  26377  chordthm  26775  dcubic  26784  lgambdd  26975  lgamucov  26976  lgamcvglem  26978  lgamcvg2  26993  fta  27018  dchrptlem2  27204  sumdchr2  27209  2sqlem11  27368  dchrisum  27431  dchrisum0flb  27449  pntibndlem3  27531  pntlemi  27543  scutbdaybnd  27757  cofsslt  27863  coinitsslt  27864  addsproplem6  27918  negsproplem6  27976  mulsproplem13  28068  mulsproplem14  28069  recsne0  28132  recsex  28158  noseqp1  28222  pjspansn  31555  chscllem3  31617  xmulcand  32899  xrge0tsmsd  33040  esumpcvgval  34089  cnpconn  35272  pconnconn  35273  connpconn  35277  pconnpi1  35279  cnllysconn  35287  cvmcov2  35317  cvmliftpht  35360  mthmpps  35624  sinccvg  35715  btwnconn1lem13  36139  neibastop2lem  36400  tailfb  36417  weiunfr  36507  unblimceq0lem  36546  knoppndvlem9  36560  knoppndvlem21  36572  knoppndvlem22  36573  matunitlindflem2  37663  poimirlem29  37695  opnmbllem0  37702  mblfinlem2  37704  mblfinlem4  37706  prdsbnd2  37841  cntotbnd  37842  heiborlem8  37864  heiborlem9  37865  cvlcvr1  39384  llnmlplnN  39584  cdlemb  39839  paddasslem10  39874  trlcnv  40210  trlator0  40216  trlid0  40221  trlnidatb  40222  cdlemd4  40246  cdlemg5  40650  trlco  40772  cdlemj3  40868  tendo0mul  40871  tendo0mulr  40872  tendoconid  40874  erngdv  41038  erngdv-rN  41046  dihmeetlem1N  41335  dihatlat  41379  hgmaprnlem5N  41945  aks6d1c5  42178  remulcan2d  42296  renegeulemv  42407  remul02  42444  remul01  42446  sn-addcand  42459  sn-addrid  42460  sn-addcan2d  42461  sn-subeu  42466  remulinvcom  42472  remullid  42473  remulcand  42478  rediveud  42482  sn-0tie0  42490  imacrhmcl  42553  fiabv  42575  prjspertr  42644  0prjspnrel  42666  acongrep  43019  jm2.27b  43045  lmhmfgsplit  43125  hbt  43169  imo72b2lem1  44208  mnuss2d  44303  mnuprdlem4  44314  mnuunid  44316  mnurndlem2  44321  cncmpmax  45075  rexlimddv2  45867  stoweidlem62  46106  salrestss  46405  oexpnegALTV  47714  oexpnegnz  47715  upciclem4  49207  aacllem  49839