Theorem rexlimddv 3140

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

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

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 3054

This theorem is referenced by:  frxp2  8123  frxp3  8130  oaabs2  8613  oemapvali  9637  cantnflem4  9645  r1pwss  9737  djuun  9879  infxpenc2lem1  9972  pwfseqlem3  10613  prlem934  10986  ltexprlem7  10995  reclem3pr  11002  00id  11349  mul02lem1  11350  addlid  11357  addcan  11358  addcan2  11359  negeu  11411  mulcand  11811  suprzcl  12614  uzwo3  12902  expmulnbnd  14200  limsupgre  15447  rlimclim1  15511  fsumcvg3  15695  oexpneg  16315  bitsfi  16407  vdwlem10  16961  mreexexlem4d  17608  mreexdomd  17610  isacs3lem  18501  grpinvalem  18600  grprida  18602  grprcan  18905  sylow1  19533  pgpfi  19535  slwhash  19554  pj1id  19629  efgsfo  19669  efgredlemc  19675  dmdprdsplitlem  19969  dpjidcl  19990  pgpfac1lem4  20010  pgpfaclem2  20014  pgpfaclem3  20015  ablsimpgcygd  20038  ablsimpgfindlem1  20039  ablsimpgfind  20042  fincygsubgodexd  20045  ablsimpgprmd  20047  gsummgp0  20227  imadrhmcl  20706  lspsolv  21053  restbas  23045  restcls  23068  restntr  23069  cnpnei  23151  cnpco  23154  pnrmopn  23230  1stcfb  23332  1stcrest  23340  2ndcctbss  23342  2ndcomap  23345  dis2ndc  23347  llyidm  23375  nllyidm  23376  hausllycmp  23381  lly1stc  23383  llycmpkgen2  23437  1stckgenlem  23440  basqtop  23598  regr1lem  23626  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  reghmph  23680  nrmhmph  23681  qtophmeo  23704  trfbas2  23730  fbasfip  23755  fbasrn  23771  trfg  23778  ssufl  23805  fmufil  23846  ufldom  23849  uffclsflim  23918  cnpfcfi  23927  alexsublem  23931  alexsubALTlem4  23937  ptcmplem3  23941  ptcmplem4  23942  tsmsxp  24042  met1stc  24409  met2ndci  24410  prdsxmslem2  24417  metcnpi3  24434  icccmplem1  24711  xrge0tsms  24723  metdseq0  24743  cnllycmp  24855  bndth  24857  lebnumlem1  24860  lebnum  24863  cfilfcls  25174  lmle  25201  relcmpcmet  25218  pjthlem2  25338  ovolscalem2  25415  ovolicc2lem4  25421  ovolicc2lem5  25422  ioombl1  25463  uniioombllem6  25489  uniioombl  25490  opnmbllem  25502  volivth  25508  mbfinf  25566  mbfi1fseqlem6  25621  itg2cnlem1  25662  itg2cn  25664  lhop2  25920  dvcnvre  25924  aareccl  26234  aaliou3lem8  26253  aaliou3lem9  26258  ulmdvlem3  26311  mtestbdd  26314  iblulm  26316  radcnvlem1  26322  abelthlem5  26345  abelthlem8  26349  chordthm  26747  dcubic  26756  lgambdd  26947  lgamucov  26948  lgamcvglem  26950  lgamcvg2  26965  fta  26990  dchrptlem2  27176  sumdchr2  27181  2sqlem11  27340  dchrisum  27403  dchrisum0flb  27421  pntibndlem3  27503  pntlemi  27515  scutbdaybnd  27727  cofsslt  27826  coinitsslt  27827  addsproplem6  27881  negsproplem6  27939  mulsproplem13  28031  mulsproplem14  28032  recsne0  28095  recsex  28121  noseqp1  28185  pjspansn  31506  chscllem3  31568  xmulcand  32841  xrge0tsmsd  33002  esumpcvgval  34068  cnpconn  35217  pconnconn  35218  connpconn  35222  pconnpi1  35224  cnllysconn  35232  cvmcov2  35262  cvmliftpht  35305  mthmpps  35569  sinccvg  35660  btwnconn1lem13  36087  neibastop2lem  36348  tailfb  36365  weiunfr  36455  unblimceq0lem  36494  knoppndvlem9  36508  knoppndvlem21  36520  knoppndvlem22  36521  matunitlindflem2  37611  poimirlem29  37643  opnmbllem0  37650  mblfinlem2  37652  mblfinlem4  37654  prdsbnd2  37789  cntotbnd  37790  heiborlem8  37812  heiborlem9  37813  cvlcvr1  39332  llnmlplnN  39533  cdlemb  39788  paddasslem10  39823  trlcnv  40159  trlator0  40165  trlid0  40170  trlnidatb  40171  cdlemd4  40195  cdlemg5  40599  trlco  40721  cdlemj3  40817  tendo0mul  40820  tendo0mulr  40821  tendoconid  40823  erngdv  40987  erngdv-rN  40995  dihmeetlem1N  41284  dihatlat  41328  hgmaprnlem5N  41894  aks6d1c5  42127  remulcan2d  42245  renegeulemv  42356  remul02  42393  remul01  42395  sn-addcand  42408  sn-addrid  42409  sn-addcan2d  42410  sn-subeu  42415  remulinvcom  42421  remullid  42422  remulcand  42427  rediveud  42431  sn-0tie0  42439  imacrhmcl  42502  fiabv  42524  prjspertr  42593  0prjspnrel  42615  acongrep  42969  jm2.27b  42995  lmhmfgsplit  43075  hbt  43119  imo72b2lem1  44158  mnuss2d  44253  mnuprdlem4  44264  mnuunid  44266  mnurndlem2  44271  cncmpmax  45026  rexlimddv2  45821  stoweidlem62  46060  salrestss  46359  oexpnegALTV  47678  oexpnegnz  47679  upciclem4  49158  aacllem  49790