Theorem rexlimddv 3162

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107  ∃wrex 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-rex 3072

This theorem is referenced by:  frxp2  8130  frxp3  8137  oaabs2  8648  oemapvali  9679  cantnflem4  9687  r1pwss  9779  djuun  9921  infxpenc2lem1  10014  pwfseqlem3  10655  prlem934  11028  ltexprlem7  11037  reclem3pr  11044  00id  11389  mul02lem1  11390  addlid  11397  addcan  11398  addcan2  11399  negeu  11450  mulcand  11847  suprzcl  12642  uzwo3  12927  expmulnbnd  14198  limsupgre  15425  rlimclim1  15489  fsumcvg3  15675  oexpneg  16288  bitsfi  16378  vdwlem10  16923  mreexexlem4d  17591  mreexdomd  17593  isacs3lem  18495  grprinvlem  18592  grprida  18594  grprcan  18858  sylow1  19471  pgpfi  19473  slwhash  19492  pj1id  19567  efgsfo  19607  efgredlemc  19613  dmdprdsplitlem  19907  dpjidcl  19928  pgpfac1lem4  19948  pgpfaclem2  19952  pgpfaclem3  19953  ablsimpgcygd  19976  ablsimpgfindlem1  19977  ablsimpgfind  19980  fincygsubgodexd  19983  ablsimpgprmd  19985  gsummgp0  20130  imadrhmcl  20413  lspsolv  20756  restbas  22662  restcls  22685  restntr  22686  cnpnei  22768  cnpco  22771  pnrmopn  22847  1stcfb  22949  1stcrest  22957  2ndcctbss  22959  2ndcomap  22962  dis2ndc  22964  llyidm  22992  nllyidm  22993  hausllycmp  22998  lly1stc  23000  llycmpkgen2  23054  1stckgenlem  23057  basqtop  23215  regr1lem  23243  kqreglem1  23245  kqreglem2  23246  kqnrmlem1  23247  kqnrmlem2  23248  reghmph  23297  nrmhmph  23298  qtophmeo  23321  trfbas2  23347  fbasfip  23372  fbasrn  23388  trfg  23395  ssufl  23422  fmufil  23463  ufldom  23466  uffclsflim  23535  cnpfcfi  23544  alexsublem  23548  alexsubALTlem4  23554  ptcmplem3  23558  ptcmplem4  23559  tsmsxp  23659  met1stc  24030  met2ndci  24031  prdsxmslem2  24038  metcnpi3  24055  icccmplem1  24338  xrge0tsms  24350  metdseq0  24370  cnllycmp  24472  bndth  24474  lebnumlem1  24477  lebnum  24480  cfilfcls  24791  lmle  24818  relcmpcmet  24835  pjthlem2  24955  ovolscalem2  25031  ovolicc2lem4  25037  ovolicc2lem5  25038  ioombl1  25079  uniioombllem6  25105  uniioombl  25106  opnmbllem  25118  volivth  25124  mbfinf  25182  mbfi1fseqlem6  25238  itg2cnlem1  25279  itg2cn  25281  lhop2  25532  dvcnvre  25536  aareccl  25839  aaliou3lem8  25858  aaliou3lem9  25863  ulmdvlem3  25914  mtestbdd  25917  iblulm  25919  radcnvlem1  25925  abelthlem5  25947  abelthlem8  25951  chordthm  26342  dcubic  26351  lgambdd  26541  lgamucov  26542  lgamcvglem  26544  lgamcvg2  26559  fta  26584  dchrptlem2  26768  sumdchr2  26773  2sqlem11  26932  dchrisum  26995  dchrisum0flb  27013  pntibndlem3  27095  pntlemi  27107  scutbdaybnd  27316  cofsslt  27405  coinitsslt  27406  addsproplem6  27458  negsproplem6  27507  mulsproplem13  27584  mulsproplem14  27585  recsex  27665  pjspansn  30830  chscllem3  30892  xmulcand  32087  xrge0tsmsd  32209  esumpcvgval  33076  cnpconn  34221  pconnconn  34222  connpconn  34226  pconnpi1  34228  cnllysconn  34236  cvmcov2  34266  cvmliftpht  34309  mthmpps  34573  sinccvg  34658  btwnconn1lem13  35071  neibastop2lem  35245  tailfb  35262  unblimceq0lem  35382  knoppndvlem9  35396  knoppndvlem21  35408  knoppndvlem22  35409  matunitlindflem2  36485  poimirlem29  36517  opnmbllem0  36524  mblfinlem2  36526  mblfinlem4  36528  prdsbnd2  36663  cntotbnd  36664  heiborlem8  36686  heiborlem9  36687  cvlcvr1  38209  llnmlplnN  38410  cdlemb  38665  paddasslem10  38700  trlcnv  39036  trlator0  39042  trlid0  39047  trlnidatb  39048  cdlemd4  39072  cdlemg5  39476  trlco  39598  cdlemj3  39694  tendo0mul  39697  tendo0mulr  39698  tendoconid  39700  erngdv  39864  erngdv-rN  39872  dihmeetlem1N  40161  dihatlat  40205  hgmaprnlem5N  40771  imacrhmcl  41089  remulcan2d  41177  renegeulemv  41241  remul02  41278  remul01  41280  sn-addcand  41292  sn-addrid  41293  sn-addcan2d  41294  sn-subeu  41299  remulinvcom  41305  remullid  41306  remulcand  41311  sn-0tie0  41312  itrere  41339  retire  41340  prjspertr  41347  0prjspnrel  41369  acongrep  41719  jm2.27b  41745  lmhmfgsplit  41828  hbt  41872  imo72b2lem1  42921  mnuss2d  43023  mnuprdlem4  43034  mnuunid  43036  mnurndlem2  43041  cncmpmax  43716  rexlimddv2  44539  stoweidlem62  44778  salrestss  45077  oexpnegALTV  46345  oexpnegnz  46346  aacllem  47848