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 395   ∈ wcel 2108  ∃wrex 3070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-rex 3071

This theorem is referenced by:  frxp2  8169  frxp3  8176  oaabs2  8687  oemapvali  9724  cantnflem4  9732  r1pwss  9824  djuun  9966  infxpenc2lem1  10059  pwfseqlem3  10700  prlem934  11073  ltexprlem7  11082  reclem3pr  11089  00id  11436  mul02lem1  11437  addlid  11444  addcan  11445  addcan2  11446  negeu  11498  mulcand  11896  suprzcl  12698  uzwo3  12985  expmulnbnd  14274  limsupgre  15517  rlimclim1  15581  fsumcvg3  15765  oexpneg  16382  bitsfi  16474  vdwlem10  17028  mreexexlem4d  17690  mreexdomd  17692  isacs3lem  18587  grpinvalem  18686  grprida  18688  grprcan  18991  sylow1  19621  pgpfi  19623  slwhash  19642  pj1id  19717  efgsfo  19757  efgredlemc  19763  dmdprdsplitlem  20057  dpjidcl  20078  pgpfac1lem4  20098  pgpfaclem2  20102  pgpfaclem3  20103  ablsimpgcygd  20126  ablsimpgfindlem1  20127  ablsimpgfind  20130  fincygsubgodexd  20133  ablsimpgprmd  20135  gsummgp0  20315  imadrhmcl  20798  lspsolv  21145  restbas  23166  restcls  23189  restntr  23190  cnpnei  23272  cnpco  23275  pnrmopn  23351  1stcfb  23453  1stcrest  23461  2ndcctbss  23463  2ndcomap  23466  dis2ndc  23468  llyidm  23496  nllyidm  23497  hausllycmp  23502  lly1stc  23504  llycmpkgen2  23558  1stckgenlem  23561  basqtop  23719  regr1lem  23747  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  reghmph  23801  nrmhmph  23802  qtophmeo  23825  trfbas2  23851  fbasfip  23876  fbasrn  23892  trfg  23899  ssufl  23926  fmufil  23967  ufldom  23970  uffclsflim  24039  cnpfcfi  24048  alexsublem  24052  alexsubALTlem4  24058  ptcmplem3  24062  ptcmplem4  24063  tsmsxp  24163  met1stc  24534  met2ndci  24535  prdsxmslem2  24542  metcnpi3  24559  icccmplem1  24844  xrge0tsms  24856  metdseq0  24876  cnllycmp  24988  bndth  24990  lebnumlem1  24993  lebnum  24996  cfilfcls  25308  lmle  25335  relcmpcmet  25352  pjthlem2  25472  ovolscalem2  25549  ovolicc2lem4  25555  ovolicc2lem5  25556  ioombl1  25597  uniioombllem6  25623  uniioombl  25624  opnmbllem  25636  volivth  25642  mbfinf  25700  mbfi1fseqlem6  25755  itg2cnlem1  25796  itg2cn  25798  lhop2  26054  dvcnvre  26058  aareccl  26368  aaliou3lem8  26387  aaliou3lem9  26392  ulmdvlem3  26445  mtestbdd  26448  iblulm  26450  radcnvlem1  26456  abelthlem5  26479  abelthlem8  26483  chordthm  26880  dcubic  26889  lgambdd  27080  lgamucov  27081  lgamcvglem  27083  lgamcvg2  27098  fta  27123  dchrptlem2  27309  sumdchr2  27314  2sqlem11  27473  dchrisum  27536  dchrisum0flb  27554  pntibndlem3  27636  pntlemi  27648  scutbdaybnd  27860  cofsslt  27952  coinitsslt  27953  addsproplem6  28007  negsproplem6  28065  mulsproplem13  28154  mulsproplem14  28155  recsex  28243  noseqp1  28297  pjspansn  31596  chscllem3  31658  xmulcand  32903  xrge0tsmsd  33065  esumpcvgval  34079  cnpconn  35235  pconnconn  35236  connpconn  35240  pconnpi1  35242  cnllysconn  35250  cvmcov2  35280  cvmliftpht  35323  mthmpps  35587  sinccvg  35678  btwnconn1lem13  36100  neibastop2lem  36361  tailfb  36378  weiunfr  36468  unblimceq0lem  36507  knoppndvlem9  36521  knoppndvlem21  36533  knoppndvlem22  36534  matunitlindflem2  37624  poimirlem29  37656  opnmbllem0  37663  mblfinlem2  37665  mblfinlem4  37667  prdsbnd2  37802  cntotbnd  37803  heiborlem8  37825  heiborlem9  37826  cvlcvr1  39340  llnmlplnN  39541  cdlemb  39796  paddasslem10  39831  trlcnv  40167  trlator0  40173  trlid0  40178  trlnidatb  40179  cdlemd4  40203  cdlemg5  40607  trlco  40729  cdlemj3  40825  tendo0mul  40828  tendo0mulr  40829  tendoconid  40831  erngdv  40995  erngdv-rN  41003  dihmeetlem1N  41292  dihatlat  41336  hgmaprnlem5N  41902  aks6d1c5  42140  remulcan2d  42298  renegeulemv  42398  remul02  42435  remul01  42437  sn-addcand  42449  sn-addrid  42450  sn-addcan2d  42451  sn-subeu  42456  remulinvcom  42462  remullid  42463  remulcand  42468  sn-0tie0  42469  sn-itrere  42498  sn-retire  42499  imacrhmcl  42524  fiabv  42546  prjspertr  42615  0prjspnrel  42637  acongrep  42992  jm2.27b  43018  lmhmfgsplit  43098  hbt  43142  imo72b2lem1  44182  mnuss2d  44283  mnuprdlem4  44294  mnuunid  44296  mnurndlem2  44301  cncmpmax  45037  rexlimddv2  45838  stoweidlem62  46077  salrestss  46376  oexpnegALTV  47664  oexpnegnz  47665  upciclem4  48926  aacllem  49320