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  8096  frxp3  8103  oaabs2  8587  oemapvali  9605  cantnflem4  9613  r1pwss  9708  djuun  9850  infxpenc2lem1  9941  pwfseqlem3  10583  prlem934  10956  ltexprlem7  10965  reclem3pr  10972  00id  11320  mul02lem1  11321  addlid  11328  addcan  11329  addcan2  11330  negeu  11382  mulcand  11782  suprzcl  12584  uzwo3  12868  expmulnbnd  14170  limsupgre  15416  rlimclim1  15480  fsumcvg3  15664  oexpneg  16284  bitsfi  16376  vdwlem10  16930  mreexexlem4d  17582  mreexdomd  17584  isacs3lem  18477  grpinvalem  18610  grprida  18612  grprcan  18915  sylow1  19544  pgpfi  19546  slwhash  19565  pj1id  19640  efgsfo  19680  efgredlemc  19686  dmdprdsplitlem  19980  dpjidcl  20001  pgpfac1lem4  20021  pgpfaclem2  20025  pgpfaclem3  20026  ablsimpgcygd  20049  ablsimpgfindlem1  20050  ablsimpgfind  20053  fincygsubgodexd  20056  ablsimpgprmd  20058  gsummgp0  20265  imadrhmcl  20742  lspsolv  21110  restbas  23114  restcls  23137  restntr  23138  cnpnei  23220  cnpco  23223  pnrmopn  23299  1stcfb  23401  1stcrest  23409  2ndcctbss  23411  2ndcomap  23414  dis2ndc  23416  llyidm  23444  nllyidm  23445  hausllycmp  23450  lly1stc  23452  llycmpkgen2  23506  1stckgenlem  23509  basqtop  23667  regr1lem  23695  kqreglem1  23697  kqreglem2  23698  kqnrmlem1  23699  kqnrmlem2  23700  reghmph  23749  nrmhmph  23750  qtophmeo  23773  trfbas2  23799  fbasfip  23824  fbasrn  23840  trfg  23847  ssufl  23874  fmufil  23915  ufldom  23918  uffclsflim  23987  cnpfcfi  23996  alexsublem  24000  alexsubALTlem4  24006  ptcmplem3  24010  ptcmplem4  24011  tsmsxp  24111  met1stc  24477  met2ndci  24478  prdsxmslem2  24485  metcnpi3  24502  icccmplem1  24779  xrge0tsms  24791  metdseq0  24811  cnllycmp  24923  bndth  24925  lebnumlem1  24928  lebnum  24931  cfilfcls  25242  lmle  25269  relcmpcmet  25286  pjthlem2  25406  ovolscalem2  25483  ovolicc2lem4  25489  ovolicc2lem5  25490  ioombl1  25531  uniioombllem6  25557  uniioombl  25558  opnmbllem  25570  volivth  25576  mbfinf  25634  mbfi1fseqlem6  25689  itg2cnlem1  25730  itg2cn  25732  lhop2  25988  dvcnvre  25992  aareccl  26302  aaliou3lem8  26321  aaliou3lem9  26326  ulmdvlem3  26379  mtestbdd  26382  iblulm  26384  radcnvlem1  26390  abelthlem5  26413  abelthlem8  26417  chordthm  26815  dcubic  26824  lgambdd  27015  lgamucov  27016  lgamcvglem  27018  lgamcvg2  27033  fta  27058  dchrptlem2  27244  sumdchr2  27249  2sqlem11  27408  dchrisum  27471  dchrisum0flb  27489  pntibndlem3  27571  pntlemi  27583  cutbdaybnd  27803  cofslts  27926  coinitslts  27927  addsproplem6  27982  negsproplem6  28041  mulsproplem13  28136  mulsproplem14  28137  recsne0  28200  recsex  28227  noseqp1  28299  pjspansn  31664  chscllem3  31726  xmulcand  33012  xrge0tsmsd  33166  esumpcvgval  34255  noinfepfnregs  35307  cnpconn  35443  pconnconn  35444  connpconn  35448  pconnpi1  35450  cnllysconn  35458  cvmcov2  35488  cvmliftpht  35531  mthmpps  35795  sinccvg  35886  btwnconn1lem13  36312  neibastop2lem  36573  tailfb  36590  weiunfr  36680  unblimceq0lem  36725  knoppndvlem9  36739  knoppndvlem21  36751  knoppndvlem22  36752  matunitlindflem2  37865  poimirlem29  37897  opnmbllem0  37904  mblfinlem2  37906  mblfinlem4  37908  prdsbnd2  38043  cntotbnd  38044  heiborlem8  38066  heiborlem9  38067  cvlcvr1  39712  llnmlplnN  39912  cdlemb  40167  paddasslem10  40202  trlcnv  40538  trlator0  40544  trlid0  40549  trlnidatb  40550  cdlemd4  40574  cdlemg5  40978  trlco  41100  cdlemj3  41196  tendo0mul  41199  tendo0mulr  41200  tendoconid  41202  erngdv  41366  erngdv-rN  41374  dihmeetlem1N  41663  dihatlat  41707  hgmaprnlem5N  42273  aks6d1c5  42506  remulcan2d  42624  renegeulemv  42735  remul02  42772  remul01  42774  sn-addcand  42787  sn-addrid  42788  sn-addcan2d  42789  sn-subeu  42794  remulinvcom  42800  remullid  42801  remulcand  42806  rediveud  42810  sn-0tie0  42818  imacrhmcl  42881  fiabv  42903  prjspertr  42960  0prjspnrel  42982  acongrep  43334  jm2.27b  43360  lmhmfgsplit  43440  hbt  43484  imo72b2lem1  44522  mnuss2d  44617  mnuprdlem4  44628  mnuunid  44630  mnurndlem2  44635  cncmpmax  45389  rexlimddv2  46178  stoweidlem62  46417  salrestss  46716  oexpnegALTV  48034  oexpnegnz  48035  upciclem4  49525  aacllem  50157