Theorem rexlimddv 3169

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144  ∃wrex 3086

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-rex 3087

This theorem is used by:  frxp2  8164  frxp3  8171  oaabs2  8662  oemapvali  9689  cantnflem4  9697  r1pwss  9795  djuun  10011  infxpenc2lem1  10102  pwfseqlem3  10749  prlem934  11122  ltexprlem7  11131  reclem3pr  11138  00id  11489  mul02lem1  11490  addlid  11497  addcan  11498  addcan2  11499  negeu  11551  mulcand  11953  suprzcl  12783  uzwo3  13074  expmulnbnd  14383  limsupgre  15654  rlimclim1  15718  fsumcvg3  15901  oexpneg  16521  bitsfi  16613  vdwlem10  17174  mreexexlem4d  17827  mreexdomd  17829  isacs3lem  18722  grpinvalem  18860  grprida  18862  grprcan  19190  sylow1  19823  pgpfi  19825  slwhash  19844  pj1id  19919  efgsfo  19959  efgredlemc  19965  dmdprdsplitlem  20259  dpjidcl  20280  pgpfac1lem4  20300  pgpfaclem2  20304  pgpfaclem3  20305  ablsimpgcygd  20328  ablsimpgfindlem1  20329  ablsimpgfind  20332  fincygsubgodexd  20335  ablsimpgprmd  20337  gsummgp0  20553  imadrhmcl  21060  lspsolv  21427  matunitlindflem2  23001  restbas  23482  restcls  23505  restntr  23506  cnpnei  23588  cnpco  23591  pnrmopn  23667  1stcfb  23769  1stcrest  23777  2ndcctbss  23780  2ndcomap  23783  dis2ndc  23785  llyidm  23813  nllyidm  23814  hausllycmp  23819  lly1stc  23821  llycmpkgen2  23875  1stckgenlem  23878  basqtop  24036  regr1lem  24064  kqreglem1  24066  kqreglem2  24067  kqnrmlem1  24068  kqnrmlem2  24069  reghmph  24118  nrmhmph  24119  qtophmeo  24142  trfbas2  24168  fbasfip  24193  fbasrn  24209  trfg  24216  ssufl  24243  fmufil  24284  ufldom  24287  uffclsflim  24356  cnpfcfi  24365  alexsublem  24369  alexsubALTlem4  24375  ptcmplem3  24379  ptcmplem4  24380  tsmsxp  24480  met1stc  24846  met2ndci  24847  prdsxmslem2  24854  metcnpi3  24871  icccmplem1  25148  xrge0tsms  25160  metdseq0  25180  cnllycmp  25283  bndth  25285  lebnumlem1  25288  lebnum  25291  cfilfcls  25601  lmle  25628  relcmpcmet  25645  pjthlem2  25765  ovolscalem2  25841  ovolicc2lem4  25847  ovolicc2lem5  25848  ioombl1  25889  uniioombllem6  25915  uniioombl  25916  opnmbllem  25928  volivth  25934  mbfinf  25992  mbfi1fseqlem6  26047  itg2cnlem1  26088  itg2cn  26090  lhop2  26341  dvcnvre  26345  preimaaa  26652  aareccl  26659  aaliou3lem8  26678  aaliou3lem9  26683  ulmdvlem3  26735  mtestbdd  26738  iblulm  26740  radcnvlem1  26746  abelthlem5  26768  abelthlem8  26772  chordthm  27171  dcubic  27180  lgambdd  27370  lgamucov  27371  lgamcvglem  27373  lgamcvg2  27388  fta  27413  dchrptlem2  27598  sumdchr2  27603  2sqlem11  27762  dchrisum  27825  dchrisum0flb  27843  pntibndlem3  27925  pntlemi  27937  cutbdaybnd  28187  cofslts  28310  coinitslts  28311  addsproplem6  28366  negsproplem6  28425  mulsproplem13  28520  mulsproplem14  28521  recsne0  28584  recsex  28611  noseqp1  28683  pjspansn  32185  chscllem3  32247  inagcgratrgxfr  33062  inagcgratrgn  33064  tgextahp  33079  xmulcand  33534  xrge0tsmsd  33681  esumpcvgval  34757  noinfepfnregs  35857  cnpconn  36082  pconnconn  36083  connpconn  36087  pconnpi1  36089  cnllysconn  36097  cvmcov2  36127  cvmliftpht  36170  mthmpps  36434  sinccvg  36525  btwnconn1lem13  36957  neibastop2lem  37241  tailfb  37258  weiunfr  37348  mh-inf3f1  37422  unblimceq0lem  37465  knoppndvlem9  37479  knoppndvlem21  37491  knoppndvlem22  37492  poimirlem29  38661  opnmbllem0  38668  mblfinlem2  38670  mblfinlem4  38672  prdsbnd2  38823  cntotbnd  38824  heiborlem8  38846  heiborlem9  38847  cvlcvr1  40490  llnmlplnN  40690  cdlemb  40945  paddasslem10  40980  trlcnv  41316  trlator0  41322  trlid0  41327  trlnidatb  41328  cdlemd4  41352  cdlemg5  41756  trlco  41878  cdlemj3  41974  tendo0mul  41977  tendo0mulr  41978  tendoconid  41980  erngdv  42144  erngdv-rN  42152  dihmeetlem1N  42441  dihatlat  42485  hgmaprnlem5N  43051  aks6d1c5  43283  remulcan2d  43401  renegeulemv  43513  remul02  43550  remul01  43552  sn-addcand  43565  sn-addrid  43566  sn-addcan2d  43567  sn-subeu  43572  remulinvcom  43578  remullid  43579  remulcand  43584  rediveud  43588  sn-0tie0  43609  imacrhmcl  43675  fiabv  43694  prjspertr  43727  prjspnnorm  43755  0prjspnrel  43757  acongrep  44081  jm2.27b  44107  lmhmfgsplit  44182  hbt  44226  imo72b2lem1  45263  mnuss2d  45342  mnuprdlem4  45353  mnuunid  45355  mnurndlem2  45360  cncmpmax  46143  rexlimddv2  46927  stoweidlem62  47166  salrestss  47465  tmachlem-agreefin  48052  oexpnegALTV  48869  oexpnegnz  48870  upciclem4  50379  aacllem  51108