Theorem rexlimddv 3143

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113  ∃wrex 3060

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-rex 3061

This theorem is referenced by:  frxp2  8086  frxp3  8093  oaabs2  8577  oemapvali  9593  cantnflem4  9601  r1pwss  9696  djuun  9838  infxpenc2lem1  9929  pwfseqlem3  10571  prlem934  10944  ltexprlem7  10953  reclem3pr  10960  00id  11308  mul02lem1  11309  addlid  11316  addcan  11317  addcan2  11318  negeu  11370  mulcand  11770  suprzcl  12572  uzwo3  12856  expmulnbnd  14158  limsupgre  15404  rlimclim1  15468  fsumcvg3  15652  oexpneg  16272  bitsfi  16364  vdwlem10  16918  mreexexlem4d  17570  mreexdomd  17572  isacs3lem  18465  grpinvalem  18598  grprida  18600  grprcan  18903  sylow1  19532  pgpfi  19534  slwhash  19553  pj1id  19628  efgsfo  19668  efgredlemc  19674  dmdprdsplitlem  19968  dpjidcl  19989  pgpfac1lem4  20009  pgpfaclem2  20013  pgpfaclem3  20014  ablsimpgcygd  20037  ablsimpgfindlem1  20038  ablsimpgfind  20041  fincygsubgodexd  20044  ablsimpgprmd  20046  gsummgp0  20253  imadrhmcl  20730  lspsolv  21098  restbas  23102  restcls  23125  restntr  23126  cnpnei  23208  cnpco  23211  pnrmopn  23287  1stcfb  23389  1stcrest  23397  2ndcctbss  23399  2ndcomap  23402  dis2ndc  23404  llyidm  23432  nllyidm  23433  hausllycmp  23438  lly1stc  23440  llycmpkgen2  23494  1stckgenlem  23497  basqtop  23655  regr1lem  23683  kqreglem1  23685  kqreglem2  23686  kqnrmlem1  23687  kqnrmlem2  23688  reghmph  23737  nrmhmph  23738  qtophmeo  23761  trfbas2  23787  fbasfip  23812  fbasrn  23828  trfg  23835  ssufl  23862  fmufil  23903  ufldom  23906  uffclsflim  23975  cnpfcfi  23984  alexsublem  23988  alexsubALTlem4  23994  ptcmplem3  23998  ptcmplem4  23999  tsmsxp  24099  met1stc  24465  met2ndci  24466  prdsxmslem2  24473  metcnpi3  24490  icccmplem1  24767  xrge0tsms  24779  metdseq0  24799  cnllycmp  24911  bndth  24913  lebnumlem1  24916  lebnum  24919  cfilfcls  25230  lmle  25257  relcmpcmet  25274  pjthlem2  25394  ovolscalem2  25471  ovolicc2lem4  25477  ovolicc2lem5  25478  ioombl1  25519  uniioombllem6  25545  uniioombl  25546  opnmbllem  25558  volivth  25564  mbfinf  25622  mbfi1fseqlem6  25677  itg2cnlem1  25718  itg2cn  25720  lhop2  25976  dvcnvre  25980  aareccl  26290  aaliou3lem8  26309  aaliou3lem9  26314  ulmdvlem3  26367  mtestbdd  26370  iblulm  26372  radcnvlem1  26378  abelthlem5  26401  abelthlem8  26405  chordthm  26803  dcubic  26812  lgambdd  27003  lgamucov  27004  lgamcvglem  27006  lgamcvg2  27021  fta  27046  dchrptlem2  27232  sumdchr2  27237  2sqlem11  27396  dchrisum  27459  dchrisum0flb  27477  pntibndlem3  27559  pntlemi  27571  cutbdaybnd  27791  cofslts  27914  coinitslts  27915  addsproplem6  27970  negsproplem6  28029  mulsproplem13  28124  mulsproplem14  28125  recsne0  28188  recsex  28215  noseqp1  28287  pjspansn  31652  chscllem3  31714  xmulcand  33002  xrge0tsmsd  33155  esumpcvgval  34235  noinfepfnregs  35288  cnpconn  35424  pconnconn  35425  connpconn  35429  pconnpi1  35431  cnllysconn  35439  cvmcov2  35469  cvmliftpht  35512  mthmpps  35776  sinccvg  35867  btwnconn1lem13  36293  neibastop2lem  36554  tailfb  36571  weiunfr  36661  unblimceq0lem  36706  knoppndvlem9  36720  knoppndvlem21  36732  knoppndvlem22  36733  matunitlindflem2  37818  poimirlem29  37850  opnmbllem0  37857  mblfinlem2  37859  mblfinlem4  37861  prdsbnd2  37996  cntotbnd  37997  heiborlem8  38019  heiborlem9  38020  cvlcvr1  39599  llnmlplnN  39799  cdlemb  40054  paddasslem10  40089  trlcnv  40425  trlator0  40431  trlid0  40436  trlnidatb  40437  cdlemd4  40461  cdlemg5  40865  trlco  40987  cdlemj3  41083  tendo0mul  41086  tendo0mulr  41087  tendoconid  41089  erngdv  41253  erngdv-rN  41261  dihmeetlem1N  41550  dihatlat  41594  hgmaprnlem5N  42160  aks6d1c5  42393  remulcan2d  42512  renegeulemv  42623  remul02  42660  remul01  42662  sn-addcand  42675  sn-addrid  42676  sn-addcan2d  42677  sn-subeu  42682  remulinvcom  42688  remullid  42689  remulcand  42694  rediveud  42698  sn-0tie0  42706  imacrhmcl  42769  fiabv  42791  prjspertr  42848  0prjspnrel  42870  acongrep  43222  jm2.27b  43248  lmhmfgsplit  43328  hbt  43372  imo72b2lem1  44410  mnuss2d  44505  mnuprdlem4  44516  mnuunid  44518  mnurndlem2  44523  cncmpmax  45277  rexlimddv2  46067  stoweidlem62  46306  salrestss  46605  oexpnegALTV  47923  oexpnegnz  47924  upciclem4  49414  aacllem  50046