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 2145  ∃wrex 3086

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 3087

This theorem is used by:  frxp2  8142  frxp3  8149  oaabs2  8637  oemapvali  9663  cantnflem4  9671  r1pwss  9766  djuun  9931  infxpenc2lem1  10022  pwfseqlem3  10669  prlem934  11042  ltexprlem7  11051  reclem3pr  11058  00id  11409  mul02lem1  11410  addlid  11417  addcan  11418  addcan2  11419  negeu  11471  mulcand  11871  suprzcl  12701  uzwo3  12992  expmulnbnd  14299  limsupgre  15568  rlimclim1  15632  fsumcvg3  15815  oexpneg  16435  bitsfi  16527  vdwlem10  17082  mreexexlem4d  17735  mreexdomd  17737  isacs3lem  18630  grpinvalem  18767  grprida  18769  grprcan  19097  sylow1  19730  pgpfi  19732  slwhash  19751  pj1id  19826  efgsfo  19866  efgredlemc  19872  dmdprdsplitlem  20166  dpjidcl  20187  pgpfac1lem4  20207  pgpfaclem2  20211  pgpfaclem3  20212  ablsimpgcygd  20235  ablsimpgfindlem1  20236  ablsimpgfind  20239  fincygsubgodexd  20242  ablsimpgprmd  20244  gsummgp0  20458  imadrhmcl  20963  lspsolv  21330  matunitlindflem2  22902  restbas  23383  restcls  23406  restntr  23407  cnpnei  23489  cnpco  23492  pnrmopn  23568  1stcfb  23670  1stcrest  23678  2ndcctbss  23681  2ndcomap  23684  dis2ndc  23686  llyidm  23714  nllyidm  23715  hausllycmp  23720  lly1stc  23722  llycmpkgen2  23776  1stckgenlem  23779  basqtop  23937  regr1lem  23965  kqreglem1  23967  kqreglem2  23968  kqnrmlem1  23969  kqnrmlem2  23970  reghmph  24019  nrmhmph  24020  qtophmeo  24043  trfbas2  24069  fbasfip  24094  fbasrn  24110  trfg  24117  ssufl  24144  fmufil  24185  ufldom  24188  uffclsflim  24257  cnpfcfi  24266  alexsublem  24270  alexsubALTlem4  24276  ptcmplem3  24280  ptcmplem4  24281  tsmsxp  24381  met1stc  24747  met2ndci  24748  prdsxmslem2  24755  metcnpi3  24772  icccmplem1  25049  xrge0tsms  25061  metdseq0  25081  cnllycmp  25184  bndth  25186  lebnumlem1  25189  lebnum  25192  cfilfcls  25502  lmle  25529  relcmpcmet  25546  pjthlem2  25666  ovolscalem2  25742  ovolicc2lem4  25748  ovolicc2lem5  25749  ioombl1  25790  uniioombllem6  25816  uniioombl  25817  opnmbllem  25829  volivth  25835  mbfinf  25893  mbfi1fseqlem6  25948  itg2cnlem1  25989  itg2cn  25991  lhop2  26242  dvcnvre  26246  preimaaa  26555  aareccl  26562  aaliou3lem8  26581  aaliou3lem9  26586  ulmdvlem3  26638  mtestbdd  26641  iblulm  26643  radcnvlem1  26649  abelthlem5  26671  abelthlem8  26675  chordthm  27074  dcubic  27083  lgambdd  27273  lgamucov  27274  lgamcvglem  27276  lgamcvg2  27291  fta  27316  dchrptlem2  27501  sumdchr2  27506  2sqlem11  27665  dchrisum  27728  dchrisum0flb  27746  pntibndlem3  27828  pntlemi  27840  cutbdaybnd  28060  cofslts  28183  coinitslts  28184  addsproplem6  28239  negsproplem6  28298  mulsproplem13  28393  mulsproplem14  28394  recsne0  28457  recsex  28484  noseqp1  28556  pjspansn  32058  chscllem3  32120  xmulcand  33366  xrge0tsmsd  33513  esumpcvgval  34588  noinfepfnregs  35658  cnpconn  35809  pconnconn  35810  connpconn  35814  pconnpi1  35816  cnllysconn  35824  cvmcov2  35854  cvmliftpht  35897  mthmpps  36161  sinccvg  36252  btwnconn1lem13  36679  neibastop2lem  36979  tailfb  36996  weiunfr  37086  unblimceq0lem  37203  knoppndvlem9  37217  knoppndvlem21  37229  knoppndvlem22  37230  poimirlem29  38398  opnmbllem0  38405  mblfinlem2  38407  mblfinlem4  38409  prdsbnd2  38545  cntotbnd  38546  heiborlem8  38568  heiborlem9  38569  cvlcvr1  40212  llnmlplnN  40412  cdlemb  40667  paddasslem10  40702  trlcnv  41038  trlator0  41044  trlid0  41049  trlnidatb  41050  cdlemd4  41074  cdlemg5  41478  trlco  41600  cdlemj3  41696  tendo0mul  41699  tendo0mulr  41700  tendoconid  41702  erngdv  41866  erngdv-rN  41874  dihmeetlem1N  42163  dihatlat  42207  hgmaprnlem5N  42773  aks6d1c5  43005  remulcan2d  43123  renegeulemv  43243  remul02  43280  remul01  43282  sn-addcand  43295  sn-addrid  43296  sn-addcan2d  43297  sn-subeu  43302  remulinvcom  43308  remullid  43309  remulcand  43314  rediveud  43318  sn-0tie0  43339  imacrhmcl  43402  fiabv  43418  prjspertr  43451  0prjspnrel  43473  acongrep  43821  jm2.27b  43847  lmhmfgsplit  43927  hbt  43971  imo72b2lem1  45009  mnuss2d  45088  mnuprdlem4  45099  mnuunid  45101  mnurndlem2  45106  cncmpmax  45866  rexlimddv2  46651  stoweidlem62  46890  salrestss  47189  tmachlem-agreefin  47776  oexpnegALTV  48593  oexpnegnz  48594  upciclem4  50095  aacllem  50772