Theorem rexlimddv 3168

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141  ∃wrex 3085

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-rex 3086

This theorem is referenced by:  frxp2  8118  frxp3  8125  oaabs2  8613  oemapvali  9633  cantnflem4  9641  r1pwss  9736  djuun  9878  infxpenc2lem1  9969  pwfseqlem3  10612  prlem934  10985  ltexprlem7  10994  reclem3pr  11001  00id  11352  mul02lem1  11353  addlid  11360  addcan  11361  addcan2  11362  negeu  11414  mulcand  11814  suprzcl  12647  uzwo3  12938  expmulnbnd  14242  limsupgre  15499  rlimclim1  15563  fsumcvg3  15747  oexpneg  16370  bitsfi  16462  vdwlem10  17017  mreexexlem4d  17670  mreexdomd  17672  isacs3lem  18565  grpinvalem  18698  grprida  18700  grprcan  19006  sylow1  19634  pgpfi  19636  slwhash  19655  pj1id  19730  efgsfo  19770  efgredlemc  19776  dmdprdsplitlem  20070  dpjidcl  20091  pgpfac1lem4  20111  pgpfaclem2  20115  pgpfaclem3  20116  ablsimpgcygd  20139  ablsimpgfindlem1  20140  ablsimpgfind  20143  fincygsubgodexd  20146  ablsimpgprmd  20148  gsummgp0  20353  imadrhmcl  20834  lspsolv  21201  restbas  23206  restcls  23229  restntr  23230  cnpnei  23312  cnpco  23315  pnrmopn  23391  1stcfb  23493  1stcrest  23501  2ndcctbss  23503  2ndcomap  23506  dis2ndc  23508  llyidm  23536  nllyidm  23537  hausllycmp  23542  lly1stc  23544  llycmpkgen2  23598  1stckgenlem  23601  basqtop  23759  regr1lem  23787  kqreglem1  23789  kqreglem2  23790  kqnrmlem1  23791  kqnrmlem2  23792  reghmph  23841  nrmhmph  23842  qtophmeo  23865  trfbas2  23891  fbasfip  23916  fbasrn  23932  trfg  23939  ssufl  23966  fmufil  24007  ufldom  24010  uffclsflim  24079  cnpfcfi  24088  alexsublem  24092  alexsubALTlem4  24098  ptcmplem3  24102  ptcmplem4  24103  tsmsxp  24203  met1stc  24569  met2ndci  24570  prdsxmslem2  24577  metcnpi3  24594  icccmplem1  24871  xrge0tsms  24883  metdseq0  24903  cnllycmp  25006  bndth  25008  lebnumlem1  25011  lebnum  25014  cfilfcls  25324  lmle  25351  relcmpcmet  25368  pjthlem2  25488  ovolscalem2  25564  ovolicc2lem4  25570  ovolicc2lem5  25571  ioombl1  25612  uniioombllem6  25638  uniioombl  25639  opnmbllem  25651  volivth  25657  mbfinf  25715  mbfi1fseqlem6  25770  itg2cnlem1  25811  itg2cn  25813  lhop2  26065  dvcnvre  26069  aareccl  26378  aaliou3lem8  26397  aaliou3lem9  26402  ulmdvlem3  26453  mtestbdd  26456  iblulm  26458  radcnvlem1  26464  abelthlem5  26486  abelthlem8  26490  chordthm  26890  dcubic  26899  lgambdd  27089  lgamucov  27090  lgamcvglem  27092  lgamcvg2  27107  fta  27132  dchrptlem2  27317  sumdchr2  27322  2sqlem11  27481  dchrisum  27544  dchrisum0flb  27562  pntibndlem3  27644  pntlemi  27656  cutbdaybnd  27876  cofslts  27999  coinitslts  28000  addsproplem6  28055  negsproplem6  28114  mulsproplem13  28209  mulsproplem14  28210  recsne0  28273  recsex  28300  noseqp1  28372  pjspansn  31737  chscllem3  31799  xmulcand  33059  xrge0tsmsd  33214  esumpcvgval  34336  noinfepfnregs  35389  cnpconn  35541  pconnconn  35542  connpconn  35546  pconnpi1  35548  cnllysconn  35556  cvmcov2  35586  cvmliftpht  35629  mthmpps  35893  sinccvg  35984  btwnconn1lem13  36410  neibastop2lem  36681  tailfb  36698  weiunfr  36788  unblimceq0lem  36905  knoppndvlem9  36919  knoppndvlem21  36931  knoppndvlem22  36932  matunitlindflem2  38077  poimirlem29  38109  opnmbllem0  38116  mblfinlem2  38118  mblfinlem4  38120  prdsbnd2  38255  cntotbnd  38256  heiborlem8  38278  heiborlem9  38279  cvlcvr1  39924  llnmlplnN  40124  cdlemb  40379  paddasslem10  40414  trlcnv  40750  trlator0  40756  trlid0  40761  trlnidatb  40762  cdlemd4  40786  cdlemg5  41190  trlco  41312  cdlemj3  41408  tendo0mul  41411  tendo0mulr  41412  tendoconid  41414  erngdv  41578  erngdv-rN  41586  dihmeetlem1N  41875  dihatlat  41919  hgmaprnlem5N  42485  aks6d1c5  42717  remulcan2d  42833  renegeulemv  42938  remul02  42975  remul01  42977  sn-addcand  42990  sn-addrid  42991  sn-addcan2d  42992  sn-subeu  42997  remulinvcom  43003  remullid  43004  remulcand  43009  rediveud  43013  sn-0tie0  43034  imacrhmcl  43097  fiabv  43115  prjspertr  43148  0prjspnrel  43170  acongrep  43518  jm2.27b  43544  lmhmfgsplit  43624  hbt  43668  imo72b2lem1  44706  mnuss2d  44801  mnuprdlem4  44812  mnuunid  44814  mnurndlem2  44819  cncmpmax  45573  rexlimddv2  46358  stoweidlem62  46597  salrestss  46896  oexpnegALTV  48260  oexpnegnz  48261  upciclem4  49751  aacllem  50383