Theorem rexlimddv 3145

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114  ∃wrex 3062

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-rex 3063

This theorem is referenced by:  frxp2  8087  frxp3  8094  oaabs2  8578  oemapvali  9596  cantnflem4  9604  r1pwss  9699  djuun  9841  infxpenc2lem1  9932  pwfseqlem3  10574  prlem934  10947  ltexprlem7  10956  reclem3pr  10963  00id  11312  mul02lem1  11313  addlid  11320  addcan  11321  addcan2  11322  negeu  11374  mulcand  11774  suprzcl  12600  uzwo3  12884  expmulnbnd  14188  limsupgre  15434  rlimclim1  15498  fsumcvg3  15682  oexpneg  16305  bitsfi  16397  vdwlem10  16952  mreexexlem4d  17604  mreexdomd  17606  isacs3lem  18499  grpinvalem  18632  grprida  18634  grprcan  18940  sylow1  19569  pgpfi  19571  slwhash  19590  pj1id  19665  efgsfo  19705  efgredlemc  19711  dmdprdsplitlem  20005  dpjidcl  20026  pgpfac1lem4  20046  pgpfaclem2  20050  pgpfaclem3  20051  ablsimpgcygd  20074  ablsimpgfindlem1  20075  ablsimpgfind  20078  fincygsubgodexd  20081  ablsimpgprmd  20083  gsummgp0  20288  imadrhmcl  20765  lspsolv  21133  restbas  23133  restcls  23156  restntr  23157  cnpnei  23239  cnpco  23242  pnrmopn  23318  1stcfb  23420  1stcrest  23428  2ndcctbss  23430  2ndcomap  23433  dis2ndc  23435  llyidm  23463  nllyidm  23464  hausllycmp  23469  lly1stc  23471  llycmpkgen2  23525  1stckgenlem  23528  basqtop  23686  regr1lem  23714  kqreglem1  23716  kqreglem2  23717  kqnrmlem1  23718  kqnrmlem2  23719  reghmph  23768  nrmhmph  23769  qtophmeo  23792  trfbas2  23818  fbasfip  23843  fbasrn  23859  trfg  23866  ssufl  23893  fmufil  23934  ufldom  23937  uffclsflim  24006  cnpfcfi  24015  alexsublem  24019  alexsubALTlem4  24025  ptcmplem3  24029  ptcmplem4  24030  tsmsxp  24130  met1stc  24496  met2ndci  24497  prdsxmslem2  24504  metcnpi3  24521  icccmplem1  24798  xrge0tsms  24810  metdseq0  24830  cnllycmp  24933  bndth  24935  lebnumlem1  24938  lebnum  24941  cfilfcls  25251  lmle  25278  relcmpcmet  25295  pjthlem2  25415  ovolscalem2  25491  ovolicc2lem4  25497  ovolicc2lem5  25498  ioombl1  25539  uniioombllem6  25565  uniioombl  25566  opnmbllem  25578  volivth  25584  mbfinf  25642  mbfi1fseqlem6  25697  itg2cnlem1  25738  itg2cn  25740  lhop2  25992  dvcnvre  25996  aareccl  26303  aaliou3lem8  26322  aaliou3lem9  26327  ulmdvlem3  26380  mtestbdd  26383  iblulm  26385  radcnvlem1  26391  abelthlem5  26413  abelthlem8  26417  chordthm  26814  dcubic  26823  lgambdd  27014  lgamucov  27015  lgamcvglem  27017  lgamcvg2  27032  fta  27057  dchrptlem2  27242  sumdchr2  27247  2sqlem11  27406  dchrisum  27469  dchrisum0flb  27487  pntibndlem3  27569  pntlemi  27581  cutbdaybnd  27801  cofslts  27924  coinitslts  27925  addsproplem6  27980  negsproplem6  28039  mulsproplem13  28134  mulsproplem14  28135  recsne0  28198  recsex  28225  noseqp1  28297  pjspansn  31663  chscllem3  31725  xmulcand  32995  xrge0tsmsd  33149  esumpcvgval  34238  noinfepfnregs  35292  cnpconn  35428  pconnconn  35429  connpconn  35433  pconnpi1  35435  cnllysconn  35443  cvmcov2  35473  cvmliftpht  35516  mthmpps  35780  sinccvg  35871  btwnconn1lem13  36297  neibastop2lem  36558  tailfb  36575  weiunfr  36665  unblimceq0lem  36782  knoppndvlem9  36796  knoppndvlem21  36808  knoppndvlem22  36809  matunitlindflem2  37952  poimirlem29  37984  opnmbllem0  37991  mblfinlem2  37993  mblfinlem4  37995  prdsbnd2  38130  cntotbnd  38131  heiborlem8  38153  heiborlem9  38154  cvlcvr1  39799  llnmlplnN  39999  cdlemb  40254  paddasslem10  40289  trlcnv  40625  trlator0  40631  trlid0  40636  trlnidatb  40637  cdlemd4  40661  cdlemg5  41065  trlco  41187  cdlemj3  41283  tendo0mul  41286  tendo0mulr  41287  tendoconid  41289  erngdv  41453  erngdv-rN  41461  dihmeetlem1N  41750  dihatlat  41794  hgmaprnlem5N  42360  aks6d1c5  42592  remulcan2d  42709  renegeulemv  42814  remul02  42851  remul01  42853  sn-addcand  42866  sn-addrid  42867  sn-addcan2d  42868  sn-subeu  42873  remulinvcom  42879  remullid  42880  remulcand  42885  rediveud  42889  sn-0tie0  42910  imacrhmcl  42973  fiabv  42995  prjspertr  43052  0prjspnrel  43074  acongrep  43426  jm2.27b  43452  lmhmfgsplit  43532  hbt  43576  imo72b2lem1  44614  mnuss2d  44709  mnuprdlem4  44720  mnuunid  44722  mnurndlem2  44727  cncmpmax  45481  rexlimddv2  46269  stoweidlem62  46508  salrestss  46807  oexpnegALTV  48165  oexpnegnz  48166  upciclem4  49656  aacllem  50288