Theorem rexlimddv 3144

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3061

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3062

This theorem is referenced by:  frxp2  8094  frxp3  8101  oaabs2  8585  oemapvali  9605  cantnflem4  9613  r1pwss  9708  djuun  9850  infxpenc2lem1  9941  pwfseqlem3  10583  prlem934  10956  ltexprlem7  10965  reclem3pr  10972  00id  11321  mul02lem1  11322  addlid  11329  addcan  11330  addcan2  11331  negeu  11383  mulcand  11783  suprzcl  12609  uzwo3  12893  expmulnbnd  14197  limsupgre  15443  rlimclim1  15507  fsumcvg3  15691  oexpneg  16314  bitsfi  16406  vdwlem10  16961  mreexexlem4d  17613  mreexdomd  17615  isacs3lem  18508  grpinvalem  18641  grprida  18643  grprcan  18949  sylow1  19578  pgpfi  19580  slwhash  19599  pj1id  19674  efgsfo  19714  efgredlemc  19720  dmdprdsplitlem  20014  dpjidcl  20035  pgpfac1lem4  20055  pgpfaclem2  20059  pgpfaclem3  20060  ablsimpgcygd  20083  ablsimpgfindlem1  20084  ablsimpgfind  20087  fincygsubgodexd  20090  ablsimpgprmd  20092  gsummgp0  20297  imadrhmcl  20774  lspsolv  21141  restbas  23123  restcls  23146  restntr  23147  cnpnei  23229  cnpco  23232  pnrmopn  23308  1stcfb  23410  1stcrest  23418  2ndcctbss  23420  2ndcomap  23423  dis2ndc  23425  llyidm  23453  nllyidm  23454  hausllycmp  23459  lly1stc  23461  llycmpkgen2  23515  1stckgenlem  23518  basqtop  23676  regr1lem  23704  kqreglem1  23706  kqreglem2  23707  kqnrmlem1  23708  kqnrmlem2  23709  reghmph  23758  nrmhmph  23759  qtophmeo  23782  trfbas2  23808  fbasfip  23833  fbasrn  23849  trfg  23856  ssufl  23883  fmufil  23924  ufldom  23927  uffclsflim  23996  cnpfcfi  24005  alexsublem  24009  alexsubALTlem4  24015  ptcmplem3  24019  ptcmplem4  24020  tsmsxp  24120  met1stc  24486  met2ndci  24487  prdsxmslem2  24494  metcnpi3  24511  icccmplem1  24788  xrge0tsms  24800  metdseq0  24820  cnllycmp  24923  bndth  24925  lebnumlem1  24928  lebnum  24931  cfilfcls  25241  lmle  25268  relcmpcmet  25285  pjthlem2  25405  ovolscalem2  25481  ovolicc2lem4  25487  ovolicc2lem5  25488  ioombl1  25529  uniioombllem6  25555  uniioombl  25556  opnmbllem  25568  volivth  25574  mbfinf  25632  mbfi1fseqlem6  25687  itg2cnlem1  25728  itg2cn  25730  lhop2  25982  dvcnvre  25986  aareccl  26292  aaliou3lem8  26311  aaliou3lem9  26316  ulmdvlem3  26367  mtestbdd  26370  iblulm  26372  radcnvlem1  26378  abelthlem5  26400  abelthlem8  26404  chordthm  26801  dcubic  26810  lgambdd  27000  lgamucov  27001  lgamcvglem  27003  lgamcvg2  27018  fta  27043  dchrptlem2  27228  sumdchr2  27233  2sqlem11  27392  dchrisum  27455  dchrisum0flb  27473  pntibndlem3  27555  pntlemi  27567  cutbdaybnd  27787  cofslts  27910  coinitslts  27911  addsproplem6  27966  negsproplem6  28025  mulsproplem13  28120  mulsproplem14  28121  recsne0  28184  recsex  28211  noseqp1  28283  pjspansn  31648  chscllem3  31710  xmulcand  32980  xrge0tsmsd  33134  esumpcvgval  34222  noinfepfnregs  35276  cnpconn  35412  pconnconn  35413  connpconn  35417  pconnpi1  35419  cnllysconn  35427  cvmcov2  35457  cvmliftpht  35500  mthmpps  35764  sinccvg  35855  btwnconn1lem13  36281  neibastop2lem  36542  tailfb  36559  weiunfr  36649  unblimceq0lem  36766  knoppndvlem9  36780  knoppndvlem21  36792  knoppndvlem22  36793  matunitlindflem2  37938  poimirlem29  37970  opnmbllem0  37977  mblfinlem2  37979  mblfinlem4  37981  prdsbnd2  38116  cntotbnd  38117  heiborlem8  38139  heiborlem9  38140  cvlcvr1  39785  llnmlplnN  39985  cdlemb  40240  paddasslem10  40275  trlcnv  40611  trlator0  40617  trlid0  40622  trlnidatb  40623  cdlemd4  40647  cdlemg5  41051  trlco  41173  cdlemj3  41269  tendo0mul  41272  tendo0mulr  41273  tendoconid  41275  erngdv  41439  erngdv-rN  41447  dihmeetlem1N  41736  dihatlat  41780  hgmaprnlem5N  42346  aks6d1c5  42578  remulcan2d  42695  renegeulemv  42800  remul02  42837  remul01  42839  sn-addcand  42852  sn-addrid  42853  sn-addcan2d  42854  sn-subeu  42859  remulinvcom  42865  remullid  42866  remulcand  42871  rediveud  42875  sn-0tie0  42896  imacrhmcl  42959  fiabv  42981  prjspertr  43038  0prjspnrel  43060  acongrep  43408  jm2.27b  43434  lmhmfgsplit  43514  hbt  43558  imo72b2lem1  44596  mnuss2d  44691  mnuprdlem4  44702  mnuunid  44704  mnurndlem2  44709  cncmpmax  45463  rexlimddv2  46251  stoweidlem62  46490  salrestss  46789  oexpnegALTV  48153  oexpnegnz  48154  upciclem4  49644  aacllem  50276