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 2113  ∃wrex 3057

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 3058

This theorem is referenced by:  frxp2  8082  frxp3  8089  oaabs2  8572  oemapvali  9583  cantnflem4  9591  r1pwss  9686  djuun  9828  infxpenc2lem1  9919  pwfseqlem3  10560  prlem934  10933  ltexprlem7  10942  reclem3pr  10949  00id  11297  mul02lem1  11298  addlid  11305  addcan  11306  addcan2  11307  negeu  11359  mulcand  11759  suprzcl  12561  uzwo3  12845  expmulnbnd  14146  limsupgre  15392  rlimclim1  15456  fsumcvg3  15640  oexpneg  16260  bitsfi  16352  vdwlem10  16906  mreexexlem4d  17557  mreexdomd  17559  isacs3lem  18452  grpinvalem  18585  grprida  18587  grprcan  18890  sylow1  19519  pgpfi  19521  slwhash  19540  pj1id  19615  efgsfo  19655  efgredlemc  19661  dmdprdsplitlem  19955  dpjidcl  19976  pgpfac1lem4  19996  pgpfaclem2  20000  pgpfaclem3  20001  ablsimpgcygd  20024  ablsimpgfindlem1  20025  ablsimpgfind  20028  fincygsubgodexd  20031  ablsimpgprmd  20033  gsummgp0  20240  imadrhmcl  20716  lspsolv  21084  restbas  23076  restcls  23099  restntr  23100  cnpnei  23182  cnpco  23185  pnrmopn  23261  1stcfb  23363  1stcrest  23371  2ndcctbss  23373  2ndcomap  23376  dis2ndc  23378  llyidm  23406  nllyidm  23407  hausllycmp  23412  lly1stc  23414  llycmpkgen2  23468  1stckgenlem  23471  basqtop  23629  regr1lem  23657  kqreglem1  23659  kqreglem2  23660  kqnrmlem1  23661  kqnrmlem2  23662  reghmph  23711  nrmhmph  23712  qtophmeo  23735  trfbas2  23761  fbasfip  23786  fbasrn  23802  trfg  23809  ssufl  23836  fmufil  23877  ufldom  23880  uffclsflim  23949  cnpfcfi  23958  alexsublem  23962  alexsubALTlem4  23968  ptcmplem3  23972  ptcmplem4  23973  tsmsxp  24073  met1stc  24439  met2ndci  24440  prdsxmslem2  24447  metcnpi3  24464  icccmplem1  24741  xrge0tsms  24753  metdseq0  24773  cnllycmp  24885  bndth  24887  lebnumlem1  24890  lebnum  24893  cfilfcls  25204  lmle  25231  relcmpcmet  25248  pjthlem2  25368  ovolscalem2  25445  ovolicc2lem4  25451  ovolicc2lem5  25452  ioombl1  25493  uniioombllem6  25519  uniioombl  25520  opnmbllem  25532  volivth  25538  mbfinf  25596  mbfi1fseqlem6  25651  itg2cnlem1  25692  itg2cn  25694  lhop2  25950  dvcnvre  25954  aareccl  26264  aaliou3lem8  26283  aaliou3lem9  26288  ulmdvlem3  26341  mtestbdd  26344  iblulm  26346  radcnvlem1  26352  abelthlem5  26375  abelthlem8  26379  chordthm  26777  dcubic  26786  lgambdd  26977  lgamucov  26978  lgamcvglem  26980  lgamcvg2  26995  fta  27020  dchrptlem2  27206  sumdchr2  27211  2sqlem11  27370  dchrisum  27433  dchrisum0flb  27451  pntibndlem3  27533  pntlemi  27545  scutbdaybnd  27759  cofsslt  27865  coinitsslt  27866  addsproplem6  27920  negsproplem6  27978  mulsproplem13  28070  mulsproplem14  28071  recsne0  28134  recsex  28160  noseqp1  28224  pjspansn  31561  chscllem3  31623  xmulcand  32910  xrge0tsmsd  33051  esumpcvgval  34114  cnpconn  35297  pconnconn  35298  connpconn  35302  pconnpi1  35304  cnllysconn  35312  cvmcov2  35342  cvmliftpht  35385  mthmpps  35649  sinccvg  35740  btwnconn1lem13  36166  neibastop2lem  36427  tailfb  36444  weiunfr  36534  unblimceq0lem  36573  knoppndvlem9  36587  knoppndvlem21  36599  knoppndvlem22  36600  matunitlindflem2  37680  poimirlem29  37712  opnmbllem0  37719  mblfinlem2  37721  mblfinlem4  37723  prdsbnd2  37858  cntotbnd  37859  heiborlem8  37881  heiborlem9  37882  cvlcvr1  39461  llnmlplnN  39661  cdlemb  39916  paddasslem10  39951  trlcnv  40287  trlator0  40293  trlid0  40298  trlnidatb  40299  cdlemd4  40323  cdlemg5  40727  trlco  40849  cdlemj3  40945  tendo0mul  40948  tendo0mulr  40949  tendoconid  40951  erngdv  41115  erngdv-rN  41123  dihmeetlem1N  41412  dihatlat  41456  hgmaprnlem5N  42022  aks6d1c5  42255  remulcan2d  42378  renegeulemv  42489  remul02  42526  remul01  42528  sn-addcand  42541  sn-addrid  42542  sn-addcan2d  42543  sn-subeu  42548  remulinvcom  42554  remullid  42555  remulcand  42560  rediveud  42564  sn-0tie0  42572  imacrhmcl  42635  fiabv  42657  prjspertr  42726  0prjspnrel  42748  acongrep  43100  jm2.27b  43126  lmhmfgsplit  43206  hbt  43250  imo72b2lem1  44289  mnuss2d  44384  mnuprdlem4  44395  mnuunid  44397  mnurndlem2  44402  cncmpmax  45156  rexlimddv2  45948  stoweidlem62  46187  salrestss  46486  oexpnegALTV  47804  oexpnegnz  47805  upciclem4  49297  aacllem  49929