Theorem rexlimddv 3178

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2149  ∃wrex 3095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-rex 3096

This theorem is referenced by:  frxp2  8136  frxp3  8143  oaabs2  8631  oemapvali  9649  cantnflem4  9657  r1pwss  9752  djuun  9908  infxpenc2lem1  9999  pwfseqlem3  10641  prlem934  11014  ltexprlem7  11023  reclem3pr  11030  00id  11381  mul02lem1  11382  addlid  11389  addcan  11390  addcan2  11391  negeu  11443  mulcand  11843  suprzcl  12672  uzwo3  12963  expmulnbnd  14267  limsupgre  15528  rlimclim1  15592  fsumcvg3  15776  oexpneg  16399  bitsfi  16491  vdwlem10  17046  mreexexlem4d  17699  mreexdomd  17701  isacs3lem  18594  grpinvalem  18727  grprida  18729  grprcan  19036  sylow1  19669  pgpfi  19671  slwhash  19690  pj1id  19765  efgsfo  19805  efgredlemc  19811  dmdprdsplitlem  20105  dpjidcl  20126  pgpfac1lem4  20146  pgpfaclem2  20150  pgpfaclem3  20151  ablsimpgcygd  20174  ablsimpgfindlem1  20175  ablsimpgfind  20178  fincygsubgodexd  20181  ablsimpgprmd  20183  gsummgp0  20395  imadrhmcl  20874  lspsolv  21241  restbas  23280  restcls  23303  restntr  23304  cnpnei  23386  cnpco  23389  pnrmopn  23465  1stcfb  23567  1stcrest  23575  2ndcctbss  23577  2ndcomap  23580  dis2ndc  23582  llyidm  23610  nllyidm  23611  hausllycmp  23616  lly1stc  23618  llycmpkgen2  23672  1stckgenlem  23675  basqtop  23833  regr1lem  23861  kqreglem1  23863  kqreglem2  23864  kqnrmlem1  23865  kqnrmlem2  23866  reghmph  23915  nrmhmph  23916  qtophmeo  23939  trfbas2  23965  fbasfip  23990  fbasrn  24006  trfg  24013  ssufl  24040  fmufil  24081  ufldom  24084  uffclsflim  24153  cnpfcfi  24162  alexsublem  24166  alexsubALTlem4  24172  ptcmplem3  24176  ptcmplem4  24177  tsmsxp  24277  met1stc  24643  met2ndci  24644  prdsxmslem2  24651  metcnpi3  24668  icccmplem1  24945  xrge0tsms  24957  metdseq0  24977  cnllycmp  25080  bndth  25082  lebnumlem1  25085  lebnum  25088  cfilfcls  25398  lmle  25425  relcmpcmet  25442  pjthlem2  25562  ovolscalem2  25638  ovolicc2lem4  25644  ovolicc2lem5  25645  ioombl1  25686  uniioombllem6  25712  uniioombl  25713  opnmbllem  25725  volivth  25731  mbfinf  25789  mbfi1fseqlem6  25844  itg2cnlem1  25885  itg2cn  25887  lhop2  26139  dvcnvre  26143  aareccl  26452  aaliou3lem8  26471  aaliou3lem9  26476  ulmdvlem3  26527  mtestbdd  26530  iblulm  26532  radcnvlem1  26538  abelthlem5  26560  abelthlem8  26564  chordthm  26964  dcubic  26973  lgambdd  27163  lgamucov  27164  lgamcvglem  27166  lgamcvg2  27181  fta  27206  dchrptlem2  27391  sumdchr2  27396  2sqlem11  27555  dchrisum  27618  dchrisum0flb  27636  pntibndlem3  27718  pntlemi  27730  cutbdaybnd  27950  cofslts  28073  coinitslts  28074  addsproplem6  28129  negsproplem6  28188  mulsproplem13  28283  mulsproplem14  28284  recsne0  28347  recsex  28374  noseqp1  28446  pjspansn  31866  chscllem3  31928  xmulcand  33177  xrge0tsmsd  33330  esumpcvgval  34409  noinfepfnregs  35464  cnpconn  35617  pconnconn  35618  connpconn  35622  pconnpi1  35624  cnllysconn  35632  cvmcov2  35662  cvmliftpht  35705  mthmpps  35969  sinccvg  36060  btwnconn1lem13  36486  neibastop2lem  36756  tailfb  36773  weiunfr  36863  unblimceq0lem  36980  knoppndvlem9  36994  knoppndvlem21  37006  knoppndvlem22  37007  matunitlindflem2  38151  poimirlem29  38183  opnmbllem0  38190  mblfinlem2  38192  mblfinlem4  38194  prdsbnd2  38329  cntotbnd  38330  heiborlem8  38352  heiborlem9  38353  cvlcvr1  39998  llnmlplnN  40198  cdlemb  40453  paddasslem10  40488  trlcnv  40824  trlator0  40830  trlid0  40835  trlnidatb  40836  cdlemd4  40860  cdlemg5  41264  trlco  41386  cdlemj3  41482  tendo0mul  41485  tendo0mulr  41486  tendoconid  41488  erngdv  41652  erngdv-rN  41660  dihmeetlem1N  41949  dihatlat  41993  hgmaprnlem5N  42559  aks6d1c5  42791  remulcan2d  42907  renegeulemv  43012  remul02  43049  remul01  43051  sn-addcand  43064  sn-addrid  43065  sn-addcan2d  43066  sn-subeu  43071  remulinvcom  43077  remullid  43078  remulcand  43083  rediveud  43087  sn-0tie0  43108  imacrhmcl  43171  fiabv  43189  prjspertr  43222  0prjspnrel  43244  acongrep  43592  jm2.27b  43618  lmhmfgsplit  43698  hbt  43742  imo72b2lem1  44780  mnuss2d  44859  mnuprdlem4  44870  mnuunid  44872  mnurndlem2  44877  cncmpmax  45637  rexlimddv2  46422  stoweidlem62  46661  salrestss  46960  oexpnegALTV  48324  oexpnegnz  48325  upciclem4  49825  aacllem  50457