Theorem rexlimddv 3170

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-rex 3088

This theorem is used by:  frxp2  8154  frxp3  8161  oaabs2  8651  oemapvali  9678  cantnflem4  9686  r1pwss  9784  djuun  10000  infxpenc2lem1  10091  pwfseqlem3  10738  prlem934  11111  ltexprlem7  11120  reclem3pr  11127  00id  11478  mul02lem1  11479  addlid  11486  addcan  11487  addcan2  11488  negeu  11540  mulcand  11942  suprzcl  12772  uzwo3  13063  expmulnbnd  14372  limsupgre  15641  rlimclim1  15705  fsumcvg3  15888  oexpneg  16508  bitsfi  16600  vdwlem10  17161  mreexexlem4d  17814  mreexdomd  17816  isacs3lem  18709  grpinvalem  18847  grprida  18849  grprcan  19177  sylow1  19810  pgpfi  19812  slwhash  19831  pj1id  19906  efgsfo  19946  efgredlemc  19952  dmdprdsplitlem  20246  dpjidcl  20267  pgpfac1lem4  20287  pgpfaclem2  20291  pgpfaclem3  20292  ablsimpgcygd  20315  ablsimpgfindlem1  20316  ablsimpgfind  20319  fincygsubgodexd  20322  ablsimpgprmd  20324  gsummgp0  20540  imadrhmcl  21047  lspsolv  21414  matunitlindflem2  22988  restbas  23469  restcls  23492  restntr  23493  cnpnei  23575  cnpco  23578  pnrmopn  23654  1stcfb  23756  1stcrest  23764  2ndcctbss  23767  2ndcomap  23770  dis2ndc  23772  llyidm  23800  nllyidm  23801  hausllycmp  23806  lly1stc  23808  llycmpkgen2  23862  1stckgenlem  23865  basqtop  24023  regr1lem  24051  kqreglem1  24053  kqreglem2  24054  kqnrmlem1  24055  kqnrmlem2  24056  reghmph  24105  nrmhmph  24106  qtophmeo  24129  trfbas2  24155  fbasfip  24180  fbasrn  24196  trfg  24203  ssufl  24230  fmufil  24271  ufldom  24274  uffclsflim  24343  cnpfcfi  24352  alexsublem  24356  alexsubALTlem4  24362  ptcmplem3  24366  ptcmplem4  24367  tsmsxp  24467  met1stc  24833  met2ndci  24834  prdsxmslem2  24841  metcnpi3  24858  icccmplem1  25135  xrge0tsms  25147  metdseq0  25167  cnllycmp  25270  bndth  25272  lebnumlem1  25275  lebnum  25278  cfilfcls  25588  lmle  25615  relcmpcmet  25632  pjthlem2  25752  ovolscalem2  25828  ovolicc2lem4  25834  ovolicc2lem5  25835  ioombl1  25876  uniioombllem6  25902  uniioombl  25903  opnmbllem  25915  volivth  25921  mbfinf  25979  mbfi1fseqlem6  26034  itg2cnlem1  26075  itg2cn  26077  lhop2  26328  dvcnvre  26332  preimaaa  26639  aareccl  26646  aaliou3lem8  26665  aaliou3lem9  26670  ulmdvlem3  26722  mtestbdd  26725  iblulm  26727  radcnvlem1  26733  abelthlem5  26755  abelthlem8  26759  chordthm  27158  dcubic  27167  lgambdd  27357  lgamucov  27358  lgamcvglem  27360  lgamcvg2  27375  fta  27400  dchrptlem2  27585  sumdchr2  27590  2sqlem11  27749  dchrisum  27812  dchrisum0flb  27830  pntibndlem3  27912  pntlemi  27924  cutbdaybnd  28174  cofslts  28297  coinitslts  28298  addsproplem6  28353  negsproplem6  28412  mulsproplem13  28507  mulsproplem14  28508  recsne0  28571  recsex  28598  noseqp1  28670  pjspansn  32172  chscllem3  32234  xmulcand  33480  xrge0tsmsd  33627  esumpcvgval  34703  noinfepfnregs  35783  cnpconn  35974  pconnconn  35975  connpconn  35979  pconnpi1  35981  cnllysconn  35989  cvmcov2  36019  cvmliftpht  36062  mthmpps  36326  sinccvg  36417  btwnconn1lem13  36844  neibastop2lem  37128  tailfb  37145  weiunfr  37235  mh-inf3f1  37309  unblimceq0lem  37352  knoppndvlem9  37366  knoppndvlem21  37378  knoppndvlem22  37379  poimirlem29  38547  opnmbllem0  38554  mblfinlem2  38556  mblfinlem4  38558  prdsbnd2  38709  cntotbnd  38710  heiborlem8  38732  heiborlem9  38733  cvlcvr1  40376  llnmlplnN  40576  cdlemb  40831  paddasslem10  40866  trlcnv  41202  trlator0  41208  trlid0  41213  trlnidatb  41214  cdlemd4  41238  cdlemg5  41642  trlco  41764  cdlemj3  41860  tendo0mul  41863  tendo0mulr  41864  tendoconid  41866  erngdv  42030  erngdv-rN  42038  dihmeetlem1N  42327  dihatlat  42371  hgmaprnlem5N  42937  aks6d1c5  43169  remulcan2d  43287  renegeulemv  43399  remul02  43436  remul01  43438  sn-addcand  43451  sn-addrid  43452  sn-addcan2d  43453  sn-subeu  43458  remulinvcom  43464  remullid  43465  remulcand  43470  rediveud  43474  sn-0tie0  43495  imacrhmcl  43561  fiabv  43580  prjspertr  43613  prjspnnorm  43641  0prjspnrel  43643  acongrep  43966  jm2.27b  43992  lmhmfgsplit  44072  hbt  44116  imo72b2lem1  45154  mnuss2d  45233  mnuprdlem4  45244  mnuunid  45246  mnurndlem2  45251  cncmpmax  46018  rexlimddv2  46802  stoweidlem62  47041  salrestss  47340  tmachlem-agreefin  47927  oexpnegALTV  48744  oexpnegnz  48745  upciclem4  50246  aacllem  50908