Theorem rexlimddv 3148

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

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

This theorem is referenced by:  frxp2  8148  frxp3  8155  oaabs2  8666  oemapvali  9703  cantnflem4  9711  r1pwss  9803  djuun  9945  infxpenc2lem1  10038  pwfseqlem3  10679  prlem934  11052  ltexprlem7  11061  reclem3pr  11068  00id  11415  mul02lem1  11416  addlid  11423  addcan  11424  addcan2  11425  negeu  11477  mulcand  11875  suprzcl  12678  uzwo3  12964  expmulnbnd  14258  limsupgre  15502  rlimclim1  15566  fsumcvg3  15750  oexpneg  16369  bitsfi  16461  vdwlem10  17015  mreexexlem4d  17664  mreexdomd  17666  isacs3lem  18557  grpinvalem  18656  grprida  18658  grprcan  18961  sylow1  19589  pgpfi  19591  slwhash  19610  pj1id  19685  efgsfo  19725  efgredlemc  19731  dmdprdsplitlem  20025  dpjidcl  20046  pgpfac1lem4  20066  pgpfaclem2  20070  pgpfaclem3  20071  ablsimpgcygd  20094  ablsimpgfindlem1  20095  ablsimpgfind  20098  fincygsubgodexd  20101  ablsimpgprmd  20103  gsummgp0  20283  imadrhmcl  20762  lspsolv  21109  restbas  23101  restcls  23124  restntr  23125  cnpnei  23207  cnpco  23210  pnrmopn  23286  1stcfb  23388  1stcrest  23396  2ndcctbss  23398  2ndcomap  23401  dis2ndc  23403  llyidm  23431  nllyidm  23432  hausllycmp  23437  lly1stc  23439  llycmpkgen2  23493  1stckgenlem  23496  basqtop  23654  regr1lem  23682  kqreglem1  23684  kqreglem2  23685  kqnrmlem1  23686  kqnrmlem2  23687  reghmph  23736  nrmhmph  23737  qtophmeo  23760  trfbas2  23786  fbasfip  23811  fbasrn  23827  trfg  23834  ssufl  23861  fmufil  23902  ufldom  23905  uffclsflim  23974  cnpfcfi  23983  alexsublem  23987  alexsubALTlem4  23993  ptcmplem3  23997  ptcmplem4  23998  tsmsxp  24098  met1stc  24465  met2ndci  24466  prdsxmslem2  24473  metcnpi3  24490  icccmplem1  24767  xrge0tsms  24779  metdseq0  24799  cnllycmp  24911  bndth  24913  lebnumlem1  24916  lebnum  24919  cfilfcls  25231  lmle  25258  relcmpcmet  25275  pjthlem2  25395  ovolscalem2  25472  ovolicc2lem4  25478  ovolicc2lem5  25479  ioombl1  25520  uniioombllem6  25546  uniioombl  25547  opnmbllem  25559  volivth  25565  mbfinf  25623  mbfi1fseqlem6  25678  itg2cnlem1  25719  itg2cn  25721  lhop2  25977  dvcnvre  25981  aareccl  26291  aaliou3lem8  26310  aaliou3lem9  26315  ulmdvlem3  26368  mtestbdd  26371  iblulm  26373  radcnvlem1  26379  abelthlem5  26402  abelthlem8  26406  chordthm  26804  dcubic  26813  lgambdd  27004  lgamucov  27005  lgamcvglem  27007  lgamcvg2  27022  fta  27047  dchrptlem2  27233  sumdchr2  27238  2sqlem11  27397  dchrisum  27460  dchrisum0flb  27478  pntibndlem3  27560  pntlemi  27572  scutbdaybnd  27784  cofsslt  27883  coinitsslt  27884  addsproplem6  27938  negsproplem6  27996  mulsproplem13  28088  mulsproplem14  28089  recsne0  28152  recsex  28178  noseqp1  28242  pjspansn  31563  chscllem3  31625  xmulcand  32900  xrge0tsmsd  33061  esumpcvgval  34114  cnpconn  35257  pconnconn  35258  connpconn  35262  pconnpi1  35264  cnllysconn  35272  cvmcov2  35302  cvmliftpht  35345  mthmpps  35609  sinccvg  35700  btwnconn1lem13  36122  neibastop2lem  36383  tailfb  36400  weiunfr  36490  unblimceq0lem  36529  knoppndvlem9  36543  knoppndvlem21  36555  knoppndvlem22  36556  matunitlindflem2  37646  poimirlem29  37678  opnmbllem0  37685  mblfinlem2  37687  mblfinlem4  37689  prdsbnd2  37824  cntotbnd  37825  heiborlem8  37847  heiborlem9  37848  cvlcvr1  39362  llnmlplnN  39563  cdlemb  39818  paddasslem10  39853  trlcnv  40189  trlator0  40195  trlid0  40200  trlnidatb  40201  cdlemd4  40225  cdlemg5  40629  trlco  40751  cdlemj3  40847  tendo0mul  40850  tendo0mulr  40851  tendoconid  40853  erngdv  41017  erngdv-rN  41025  dihmeetlem1N  41314  dihatlat  41358  hgmaprnlem5N  41924  aks6d1c5  42157  remulcan2d  42275  renegeulemv  42386  remul02  42423  remul01  42425  sn-addcand  42437  sn-addrid  42438  sn-addcan2d  42439  sn-subeu  42444  remulinvcom  42450  remullid  42451  remulcand  42456  sn-0tie0  42457  sn-itrere  42486  sn-retire  42487  imacrhmcl  42512  fiabv  42534  prjspertr  42603  0prjspnrel  42625  acongrep  42979  jm2.27b  43005  lmhmfgsplit  43085  hbt  43129  imo72b2lem1  44168  mnuss2d  44263  mnuprdlem4  44274  mnuunid  44276  mnurndlem2  44281  cncmpmax  45036  rexlimddv2  45832  stoweidlem62  46071  salrestss  46370  oexpnegALTV  47671  oexpnegnz  47672  upciclem4  49084  aacllem  49645