Theorem rexlimddv 3161

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106  ∃wrex 3070

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 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3071

This theorem is referenced by:  frxp2  8132  frxp3  8139  oaabs2  8650  oemapvali  9681  cantnflem4  9689  r1pwss  9781  djuun  9923  infxpenc2lem1  10016  pwfseqlem3  10657  prlem934  11030  ltexprlem7  11039  reclem3pr  11046  00id  11391  mul02lem1  11392  addlid  11399  addcan  11400  addcan2  11401  negeu  11452  mulcand  11849  suprzcl  12644  uzwo3  12929  expmulnbnd  14200  limsupgre  15427  rlimclim1  15491  fsumcvg3  15677  oexpneg  16290  bitsfi  16380  vdwlem10  16925  mreexexlem4d  17593  mreexdomd  17595  isacs3lem  18497  grprinvlem  18594  grprida  18596  grprcan  18860  sylow1  19473  pgpfi  19475  slwhash  19494  pj1id  19569  efgsfo  19609  efgredlemc  19615  dmdprdsplitlem  19909  dpjidcl  19930  pgpfac1lem4  19950  pgpfaclem2  19954  pgpfaclem3  19955  ablsimpgcygd  19978  ablsimpgfindlem1  19979  ablsimpgfind  19982  fincygsubgodexd  19985  ablsimpgprmd  19987  gsummgp0  20134  imadrhmcl  20417  lspsolv  20762  restbas  22669  restcls  22692  restntr  22693  cnpnei  22775  cnpco  22778  pnrmopn  22854  1stcfb  22956  1stcrest  22964  2ndcctbss  22966  2ndcomap  22969  dis2ndc  22971  llyidm  22999  nllyidm  23000  hausllycmp  23005  lly1stc  23007  llycmpkgen2  23061  1stckgenlem  23064  basqtop  23222  regr1lem  23250  kqreglem1  23252  kqreglem2  23253  kqnrmlem1  23254  kqnrmlem2  23255  reghmph  23304  nrmhmph  23305  qtophmeo  23328  trfbas2  23354  fbasfip  23379  fbasrn  23395  trfg  23402  ssufl  23429  fmufil  23470  ufldom  23473  uffclsflim  23542  cnpfcfi  23551  alexsublem  23555  alexsubALTlem4  23561  ptcmplem3  23565  ptcmplem4  23566  tsmsxp  23666  met1stc  24037  met2ndci  24038  prdsxmslem2  24045  metcnpi3  24062  icccmplem1  24345  xrge0tsms  24357  metdseq0  24377  cnllycmp  24479  bndth  24481  lebnumlem1  24484  lebnum  24487  cfilfcls  24798  lmle  24825  relcmpcmet  24842  pjthlem2  24962  ovolscalem2  25038  ovolicc2lem4  25044  ovolicc2lem5  25045  ioombl1  25086  uniioombllem6  25112  uniioombl  25113  opnmbllem  25125  volivth  25131  mbfinf  25189  mbfi1fseqlem6  25245  itg2cnlem1  25286  itg2cn  25288  lhop2  25539  dvcnvre  25543  aareccl  25846  aaliou3lem8  25865  aaliou3lem9  25870  ulmdvlem3  25921  mtestbdd  25924  iblulm  25926  radcnvlem1  25932  abelthlem5  25954  abelthlem8  25958  chordthm  26349  dcubic  26358  lgambdd  26548  lgamucov  26549  lgamcvglem  26551  lgamcvg2  26566  fta  26591  dchrptlem2  26775  sumdchr2  26780  2sqlem11  26939  dchrisum  27002  dchrisum0flb  27020  pntibndlem3  27102  pntlemi  27114  scutbdaybnd  27324  cofsslt  27414  coinitsslt  27415  addsproplem6  27467  negsproplem6  27517  mulsproplem13  27594  mulsproplem14  27595  recsex  27675  pjspansn  30868  chscllem3  30930  xmulcand  32125  xrge0tsmsd  32250  esumpcvgval  33145  cnpconn  34290  pconnconn  34291  connpconn  34295  pconnpi1  34297  cnllysconn  34305  cvmcov2  34335  cvmliftpht  34378  mthmpps  34642  sinccvg  34727  btwnconn1lem13  35140  neibastop2lem  35331  tailfb  35348  unblimceq0lem  35468  knoppndvlem9  35482  knoppndvlem21  35494  knoppndvlem22  35495  matunitlindflem2  36571  poimirlem29  36603  opnmbllem0  36610  mblfinlem2  36612  mblfinlem4  36614  prdsbnd2  36749  cntotbnd  36750  heiborlem8  36772  heiborlem9  36773  cvlcvr1  38295  llnmlplnN  38496  cdlemb  38751  paddasslem10  38786  trlcnv  39122  trlator0  39128  trlid0  39133  trlnidatb  39134  cdlemd4  39158  cdlemg5  39562  trlco  39684  cdlemj3  39780  tendo0mul  39783  tendo0mulr  39784  tendoconid  39786  erngdv  39950  erngdv-rN  39958  dihmeetlem1N  40247  dihatlat  40291  hgmaprnlem5N  40857  imacrhmcl  41173  remulcan2d  41259  renegeulemv  41323  remul02  41360  remul01  41362  sn-addcand  41374  sn-addrid  41375  sn-addcan2d  41376  sn-subeu  41381  remulinvcom  41387  remullid  41388  remulcand  41393  sn-0tie0  41394  itrere  41421  retire  41422  prjspertr  41429  0prjspnrel  41451  acongrep  41801  jm2.27b  41827  lmhmfgsplit  41910  hbt  41954  imo72b2lem1  43003  mnuss2d  43105  mnuprdlem4  43116  mnuunid  43118  mnurndlem2  43123  cncmpmax  43798  rexlimddv2  44618  stoweidlem62  44857  salrestss  45156  oexpnegALTV  46424  oexpnegnz  46425  aacllem  47926