Theorem rexlimddv 3174

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146  ∃wrex 3091

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3092

This theorem is used by:  frxp2  8142  frxp3  8149  oaabs2  8637  oemapvali  9656  cantnflem4  9664  r1pwss  9759  djuun  9924  infxpenc2lem1  10015  pwfseqlem3  10656  prlem934  11029  ltexprlem7  11038  reclem3pr  11045  00id  11396  mul02lem1  11397  addlid  11404  addcan  11405  addcan2  11406  negeu  11458  mulcand  11858  suprzcl  12687  uzwo3  12978  expmulnbnd  14284  limsupgre  15551  rlimclim1  15615  fsumcvg3  15798  oexpneg  16420  bitsfi  16512  vdwlem10  17067  mreexexlem4d  17720  mreexdomd  17722  isacs3lem  18615  grpinvalem  18749  grprida  18751  grprcan  19063  sylow1  19696  pgpfi  19698  slwhash  19717  pj1id  19792  efgsfo  19832  efgredlemc  19838  dmdprdsplitlem  20132  dpjidcl  20153  pgpfac1lem4  20173  pgpfaclem2  20177  pgpfaclem3  20178  ablsimpgcygd  20201  ablsimpgfindlem1  20202  ablsimpgfind  20205  fincygsubgodexd  20208  ablsimpgprmd  20210  gsummgp0  20424  imadrhmcl  20929  lspsolv  21296  restbas  23344  restcls  23367  restntr  23368  cnpnei  23450  cnpco  23453  pnrmopn  23529  1stcfb  23631  1stcrest  23639  2ndcctbss  23641  2ndcomap  23644  dis2ndc  23646  llyidm  23674  nllyidm  23675  hausllycmp  23680  lly1stc  23682  llycmpkgen2  23736  1stckgenlem  23739  basqtop  23897  regr1lem  23925  kqreglem1  23927  kqreglem2  23928  kqnrmlem1  23929  kqnrmlem2  23930  reghmph  23979  nrmhmph  23980  qtophmeo  24003  trfbas2  24029  fbasfip  24054  fbasrn  24070  trfg  24077  ssufl  24104  fmufil  24145  ufldom  24148  uffclsflim  24217  cnpfcfi  24226  alexsublem  24230  alexsubALTlem4  24236  ptcmplem3  24240  ptcmplem4  24241  tsmsxp  24341  met1stc  24707  met2ndci  24708  prdsxmslem2  24715  metcnpi3  24732  icccmplem1  25009  xrge0tsms  25021  metdseq0  25041  cnllycmp  25144  bndth  25146  lebnumlem1  25149  lebnum  25152  cfilfcls  25462  lmle  25489  relcmpcmet  25506  pjthlem2  25626  ovolscalem2  25702  ovolicc2lem4  25708  ovolicc2lem5  25709  ioombl1  25750  uniioombllem6  25776  uniioombl  25777  opnmbllem  25789  volivth  25795  mbfinf  25853  mbfi1fseqlem6  25908  itg2cnlem1  25949  itg2cn  25951  lhop2  26203  dvcnvre  26207  aareccl  26518  aaliou3lem8  26537  aaliou3lem9  26542  ulmdvlem3  26594  mtestbdd  26597  iblulm  26599  radcnvlem1  26605  abelthlem5  26627  abelthlem8  26631  chordthm  27031  dcubic  27040  lgambdd  27230  lgamucov  27231  lgamcvglem  27233  lgamcvg2  27248  fta  27273  dchrptlem2  27458  sumdchr2  27463  2sqlem11  27622  dchrisum  27685  dchrisum0flb  27703  pntibndlem3  27785  pntlemi  27797  cutbdaybnd  28017  cofslts  28140  coinitslts  28141  addsproplem6  28196  negsproplem6  28255  mulsproplem13  28350  mulsproplem14  28351  recsne0  28414  recsex  28441  noseqp1  28513  pjspansn  31958  chscllem3  32020  xmulcand  33269  xrge0tsmsd  33416  esumpcvgval  34491  noinfepfnregs  35561  cnpconn  35735  pconnconn  35736  connpconn  35740  pconnpi1  35742  cnllysconn  35750  cvmcov2  35780  cvmliftpht  35823  mthmpps  36087  sinccvg  36178  btwnconn1lem13  36604  neibastop2lem  36904  tailfb  36921  weiunfr  37011  unblimceq0lem  37128  knoppndvlem9  37142  knoppndvlem21  37154  knoppndvlem22  37155  matunitlindflem2  38301  poimirlem29  38333  opnmbllem0  38340  mblfinlem2  38342  mblfinlem4  38344  prdsbnd2  38479  cntotbnd  38480  heiborlem8  38502  heiborlem9  38503  cvlcvr1  40146  llnmlplnN  40346  cdlemb  40601  paddasslem10  40636  trlcnv  40972  trlator0  40978  trlid0  40983  trlnidatb  40984  cdlemd4  41008  cdlemg5  41412  trlco  41534  cdlemj3  41630  tendo0mul  41633  tendo0mulr  41634  tendoconid  41636  erngdv  41800  erngdv-rN  41808  dihmeetlem1N  42097  dihatlat  42141  hgmaprnlem5N  42707  aks6d1c5  42939  remulcan2d  43057  renegeulemv  43162  remul02  43199  remul01  43201  sn-addcand  43214  sn-addrid  43215  sn-addcan2d  43216  sn-subeu  43221  remulinvcom  43227  remullid  43228  remulcand  43233  rediveud  43237  sn-0tie0  43258  imacrhmcl  43321  fiabv  43337  prjspertr  43370  0prjspnrel  43392  acongrep  43740  jm2.27b  43766  lmhmfgsplit  43846  hbt  43890  imo72b2lem1  44928  mnuss2d  45007  mnuprdlem4  45018  mnuunid  45020  mnurndlem2  45025  cncmpmax  45785  rexlimddv2  46570  stoweidlem62  46809  salrestss  47108  oexpnegALTV  48475  oexpnegnz  48476  upciclem4  49980  aacllem  50654