Theorem rexlimddv 3167

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108  ∃wrex 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-rex 3077

This theorem is referenced by:  frxp2  8185  frxp3  8192  oaabs2  8705  oemapvali  9753  cantnflem4  9761  r1pwss  9853  djuun  9995  infxpenc2lem1  10088  pwfseqlem3  10729  prlem934  11102  ltexprlem7  11111  reclem3pr  11118  00id  11465  mul02lem1  11466  addlid  11473  addcan  11474  addcan2  11475  negeu  11526  mulcand  11923  suprzcl  12723  uzwo3  13008  expmulnbnd  14284  limsupgre  15527  rlimclim1  15591  fsumcvg3  15777  oexpneg  16393  bitsfi  16483  vdwlem10  17037  mreexexlem4d  17705  mreexdomd  17707  isacs3lem  18612  grpinvalem  18711  grprida  18713  grprcan  19013  sylow1  19645  pgpfi  19647  slwhash  19666  pj1id  19741  efgsfo  19781  efgredlemc  19787  dmdprdsplitlem  20081  dpjidcl  20102  pgpfac1lem4  20122  pgpfaclem2  20126  pgpfaclem3  20127  ablsimpgcygd  20150  ablsimpgfindlem1  20151  ablsimpgfind  20154  fincygsubgodexd  20157  ablsimpgprmd  20159  gsummgp0  20341  imadrhmcl  20820  lspsolv  21168  restbas  23187  restcls  23210  restntr  23211  cnpnei  23293  cnpco  23296  pnrmopn  23372  1stcfb  23474  1stcrest  23482  2ndcctbss  23484  2ndcomap  23487  dis2ndc  23489  llyidm  23517  nllyidm  23518  hausllycmp  23523  lly1stc  23525  llycmpkgen2  23579  1stckgenlem  23582  basqtop  23740  regr1lem  23768  kqreglem1  23770  kqreglem2  23771  kqnrmlem1  23772  kqnrmlem2  23773  reghmph  23822  nrmhmph  23823  qtophmeo  23846  trfbas2  23872  fbasfip  23897  fbasrn  23913  trfg  23920  ssufl  23947  fmufil  23988  ufldom  23991  uffclsflim  24060  cnpfcfi  24069  alexsublem  24073  alexsubALTlem4  24079  ptcmplem3  24083  ptcmplem4  24084  tsmsxp  24184  met1stc  24555  met2ndci  24556  prdsxmslem2  24563  metcnpi3  24580  icccmplem1  24863  xrge0tsms  24875  metdseq0  24895  cnllycmp  25007  bndth  25009  lebnumlem1  25012  lebnum  25015  cfilfcls  25327  lmle  25354  relcmpcmet  25371  pjthlem2  25491  ovolscalem2  25568  ovolicc2lem4  25574  ovolicc2lem5  25575  ioombl1  25616  uniioombllem6  25642  uniioombl  25643  opnmbllem  25655  volivth  25661  mbfinf  25719  mbfi1fseqlem6  25775  itg2cnlem1  25816  itg2cn  25818  lhop2  26074  dvcnvre  26078  aareccl  26386  aaliou3lem8  26405  aaliou3lem9  26410  ulmdvlem3  26463  mtestbdd  26466  iblulm  26468  radcnvlem1  26474  abelthlem5  26497  abelthlem8  26501  chordthm  26898  dcubic  26907  lgambdd  27098  lgamucov  27099  lgamcvglem  27101  lgamcvg2  27116  fta  27141  dchrptlem2  27327  sumdchr2  27332  2sqlem11  27491  dchrisum  27554  dchrisum0flb  27572  pntibndlem3  27654  pntlemi  27666  scutbdaybnd  27878  cofsslt  27970  coinitsslt  27971  addsproplem6  28025  negsproplem6  28083  mulsproplem13  28172  mulsproplem14  28173  recsex  28261  noseqp1  28315  pjspansn  31609  chscllem3  31671  xmulcand  32885  xrge0tsmsd  33041  esumpcvgval  34042  cnpconn  35198  pconnconn  35199  connpconn  35203  pconnpi1  35205  cnllysconn  35213  cvmcov2  35243  cvmliftpht  35286  mthmpps  35550  sinccvg  35641  btwnconn1lem13  36063  neibastop2lem  36326  tailfb  36343  weiunfr  36433  unblimceq0lem  36472  knoppndvlem9  36486  knoppndvlem21  36498  knoppndvlem22  36499  matunitlindflem2  37577  poimirlem29  37609  opnmbllem0  37616  mblfinlem2  37618  mblfinlem4  37620  prdsbnd2  37755  cntotbnd  37756  heiborlem8  37778  heiborlem9  37779  cvlcvr1  39295  llnmlplnN  39496  cdlemb  39751  paddasslem10  39786  trlcnv  40122  trlator0  40128  trlid0  40133  trlnidatb  40134  cdlemd4  40158  cdlemg5  40562  trlco  40684  cdlemj3  40780  tendo0mul  40783  tendo0mulr  40784  tendoconid  40786  erngdv  40950  erngdv-rN  40958  dihmeetlem1N  41247  dihatlat  41291  hgmaprnlem5N  41857  aks6d1c5  42096  remulcan2d  42252  renegeulemv  42344  remul02  42381  remul01  42383  sn-addcand  42395  sn-addrid  42396  sn-addcan2d  42397  sn-subeu  42402  remulinvcom  42408  remullid  42409  remulcand  42414  sn-0tie0  42415  sn-itrere  42444  sn-retire  42445  imacrhmcl  42469  fiabv  42491  prjspertr  42560  0prjspnrel  42582  acongrep  42937  jm2.27b  42963  lmhmfgsplit  43043  hbt  43087  imo72b2lem1  44131  mnuss2d  44233  mnuprdlem4  44244  mnuunid  44246  mnurndlem2  44251  cncmpmax  44932  rexlimddv2  45744  stoweidlem62  45983  salrestss  46282  oexpnegALTV  47551  oexpnegnz  47552  aacllem  48895