Theorem rexlimddv 3158

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105  ∃wrex 3067

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-rex 3068

This theorem is referenced by:  frxp2  8167  frxp3  8174  oaabs2  8685  oemapvali  9721  cantnflem4  9729  r1pwss  9821  djuun  9963  infxpenc2lem1  10056  pwfseqlem3  10697  prlem934  11070  ltexprlem7  11079  reclem3pr  11086  00id  11433  mul02lem1  11434  addlid  11441  addcan  11442  addcan2  11443  negeu  11495  mulcand  11893  suprzcl  12695  uzwo3  12982  expmulnbnd  14270  limsupgre  15513  rlimclim1  15577  fsumcvg3  15761  oexpneg  16378  bitsfi  16470  vdwlem10  17023  mreexexlem4d  17691  mreexdomd  17693  isacs3lem  18599  grpinvalem  18698  grprida  18700  grprcan  19003  sylow1  19635  pgpfi  19637  slwhash  19656  pj1id  19731  efgsfo  19771  efgredlemc  19777  dmdprdsplitlem  20071  dpjidcl  20092  pgpfac1lem4  20112  pgpfaclem2  20116  pgpfaclem3  20117  ablsimpgcygd  20140  ablsimpgfindlem1  20141  ablsimpgfind  20144  fincygsubgodexd  20147  ablsimpgprmd  20149  gsummgp0  20331  imadrhmcl  20814  lspsolv  21162  restbas  23181  restcls  23204  restntr  23205  cnpnei  23287  cnpco  23290  pnrmopn  23366  1stcfb  23468  1stcrest  23476  2ndcctbss  23478  2ndcomap  23481  dis2ndc  23483  llyidm  23511  nllyidm  23512  hausllycmp  23517  lly1stc  23519  llycmpkgen2  23573  1stckgenlem  23576  basqtop  23734  regr1lem  23762  kqreglem1  23764  kqreglem2  23765  kqnrmlem1  23766  kqnrmlem2  23767  reghmph  23816  nrmhmph  23817  qtophmeo  23840  trfbas2  23866  fbasfip  23891  fbasrn  23907  trfg  23914  ssufl  23941  fmufil  23982  ufldom  23985  uffclsflim  24054  cnpfcfi  24063  alexsublem  24067  alexsubALTlem4  24073  ptcmplem3  24077  ptcmplem4  24078  tsmsxp  24178  met1stc  24549  met2ndci  24550  prdsxmslem2  24557  metcnpi3  24574  icccmplem1  24857  xrge0tsms  24869  metdseq0  24889  cnllycmp  25001  bndth  25003  lebnumlem1  25006  lebnum  25009  cfilfcls  25321  lmle  25348  relcmpcmet  25365  pjthlem2  25485  ovolscalem2  25562  ovolicc2lem4  25568  ovolicc2lem5  25569  ioombl1  25610  uniioombllem6  25636  uniioombl  25637  opnmbllem  25649  volivth  25655  mbfinf  25713  mbfi1fseqlem6  25769  itg2cnlem1  25810  itg2cn  25812  lhop2  26068  dvcnvre  26072  aareccl  26382  aaliou3lem8  26401  aaliou3lem9  26406  ulmdvlem3  26459  mtestbdd  26462  iblulm  26464  radcnvlem1  26470  abelthlem5  26493  abelthlem8  26497  chordthm  26894  dcubic  26903  lgambdd  27094  lgamucov  27095  lgamcvglem  27097  lgamcvg2  27112  fta  27137  dchrptlem2  27323  sumdchr2  27328  2sqlem11  27487  dchrisum  27550  dchrisum0flb  27568  pntibndlem3  27650  pntlemi  27662  scutbdaybnd  27874  cofsslt  27966  coinitsslt  27967  addsproplem6  28021  negsproplem6  28079  mulsproplem13  28168  mulsproplem14  28169  recsex  28257  noseqp1  28311  pjspansn  31605  chscllem3  31667  xmulcand  32887  xrge0tsmsd  33047  esumpcvgval  34058  cnpconn  35214  pconnconn  35215  connpconn  35219  pconnpi1  35221  cnllysconn  35229  cvmcov2  35259  cvmliftpht  35302  mthmpps  35566  sinccvg  35657  btwnconn1lem13  36080  neibastop2lem  36342  tailfb  36359  weiunfr  36449  unblimceq0lem  36488  knoppndvlem9  36502  knoppndvlem21  36514  knoppndvlem22  36515  matunitlindflem2  37603  poimirlem29  37635  opnmbllem0  37642  mblfinlem2  37644  mblfinlem4  37646  prdsbnd2  37781  cntotbnd  37782  heiborlem8  37804  heiborlem9  37805  cvlcvr1  39320  llnmlplnN  39521  cdlemb  39776  paddasslem10  39811  trlcnv  40147  trlator0  40153  trlid0  40158  trlnidatb  40159  cdlemd4  40183  cdlemg5  40587  trlco  40709  cdlemj3  40805  tendo0mul  40808  tendo0mulr  40809  tendoconid  40811  erngdv  40975  erngdv-rN  40983  dihmeetlem1N  41272  dihatlat  41316  hgmaprnlem5N  41882  aks6d1c5  42120  remulcan2d  42276  renegeulemv  42374  remul02  42411  remul01  42413  sn-addcand  42425  sn-addrid  42426  sn-addcan2d  42427  sn-subeu  42432  remulinvcom  42438  remullid  42439  remulcand  42444  sn-0tie0  42445  sn-itrere  42474  sn-retire  42475  imacrhmcl  42500  fiabv  42522  prjspertr  42591  0prjspnrel  42613  acongrep  42968  jm2.27b  42994  lmhmfgsplit  43074  hbt  43118  imo72b2lem1  44158  mnuss2d  44259  mnuprdlem4  44270  mnuunid  44272  mnurndlem2  44277  cncmpmax  44969  rexlimddv2  45778  stoweidlem62  46017  salrestss  46316  oexpnegALTV  47601  oexpnegnz  47602  upciclem4  48814  aacllem  49031