Theorem exlimddv 1938

Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1933). (Contributed by Mario Carneiro, 15-Jun-2016.)

Hypotheses

Ref	Expression
exlimddv.1	⊢ (𝜑 → ∃𝑥𝜓)
exlimddv.2	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
exlimddv	⊢ (𝜑 → 𝜒)

Distinct variable groups:   𝜒,𝑥   𝜑,𝑥

Allowed substitution hint:   𝜓(𝑥)

Proof of Theorem exlimddv

Step	Hyp	Ref	Expression
1		exlimddv.1	. 2 ⊢ (𝜑 → ∃𝑥𝜓)
2		exlimddv.2	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	2	ex 413	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1936	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 396  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782

This theorem is referenced by:  vtocld  3542  fvmptdv2  7016  fprresex  8297  wfrlem17OLD  8327  tfrlem9a  8388  erref  8725  domdifsn  9056  xpdom2  9069  enfixsn  9083  sucdom2OLD  9084  domunsn  9129  mapdom1  9144  sucdom2  9208  fineqvlem  9264  fissuni  9359  fipreima  9360  indexfi  9362  brwdom2  9570  wdomtr  9572  unwdomg  9581  unxpwdom  9586  infdifsn  9654  isinffi  9989  ac5num  10033  numacn  10046  acndom  10048  acndom2  10051  fodomacn  10053  infpss  10214  ssfin4  10307  domfin4  10308  enfin2i  10318  fin23lem31  10340  fin23lem41  10349  axcclem  10454  canthp1lem1  10649  canthp1  10651  winafp  10694  wun0  10715  prlem936  11044  supmul  12188  supxrre  13308  infxrre  13317  ixxub  13347  ixxlb  13348  hash1elsn  14333  relexpindlem  15012  isumltss  15796  eulerth  16718  ramub2  16949  mrieqv2d  17585  mreexexlem4d  17593  acsinfd  18511  acsdomd  18512  dfgrp3lem  18923  issubg2  19023  psgnunilem3  19366  sylow1lem4  19471  sylow3  19503  prmcyg  19764  ablfaclem3  19959  lbspss  20698  lsmcv  20760  cygzn  21132  lbslcic  21402  lmff  22812  tgcmp  22912  hauscmplem  22917  clsconn  22941  2ndcsep  22970  1stcelcls  22972  ptcnplem  23132  txcn  23137  fbdmn0  23345  ptcmplem2  23564  ptcmplem3  23565  tsmsxplem1  23664  met2ndci  24038  nmoid  24266  phtpcer  24518  phtpcco2  24522  cmetcau  24813  iscmet3lem2  24816  bcthlem4  24851  bcthlem5  24852  ovolicc2lem2  25042  vitali  25137  mbfimaopnlem  25179  limciun  25418  vieta1lem2  25831  tgldim0eq  27792  hpgerlem  28054  cusgrfi  28753  fusgrmaxsize  28759  minvecolem5  30172  foresf1o  31780  unidifsnel  31810  unidifsnne  31811  2ndimaxp  31910  aciunf1lem  31925  fsumiunle  32073  cycpmconjslem2  32355  cycpmconjs  32356  elrspunidl  32591  qsdrng  32656  dimcl  32746  lmimdim  32747  lmicdim  32748  lvecdim0i  32749  lvecdim0  32750  lssdimle  32751  dimpropd  32752  dimkerim  32771  fedgmul  32775  extdg1id  32801  locfinref  32890  esumcst  33130  esumiun  33161  unelldsys  33225  sigapildsys  33229  carsggect  33386  carsgclctunlem3  33388  erdsze2lem1  34263  erdsze2  34265  ptpconn  34293  cvmliftpht  34378  filnetlem3  35351  exlimimd  36310  poimirlem32  36606  mblfinlem2  36612  mblfinlem3  36613  mblfinlem4  36614  sdclem1  36697  sstotbnd  36729  prdsbnd  36747  prdstotbnd  36748  heibor1lem  36763  bfp  36778  eqvrelref  37566  llnn0  38473  lplnn0N  38504  lvoln0N  38548  diaglbN  40012  diaintclN  40015  dibglbN  40123  dibintclN  40124  dihglblem2aN  40250  dihintcl  40301  dvh1dim  40399  sticksstones20  41068  eldioph2lem1  41580  eldioph2lem2  41581  rencldnfilem  41640  kelac1  41887  hbt  41954  cpcoll2d  43100  cncmpmax  43798  lptre2pt  44435  itgsubsticclem  44770  stoweidlem28  44823  stoweidlem31  44826  stoweidlem46  44841  stoweidlem53  44848  stoweidlem59  44854  uniimaelsetpreimafv  46143  setrec1  47814