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  7013  fprresex  8291  wfrlem17OLD  8321  tfrlem9a  8382  erref  8719  domdifsn  9050  xpdom2  9063  enfixsn  9077  sucdom2OLD  9078  domunsn  9123  mapdom1  9138  sucdom2  9202  fineqvlem  9258  fissuni  9353  fipreima  9354  indexfi  9356  brwdom2  9564  wdomtr  9566  unwdomg  9575  unxpwdom  9580  infdifsn  9648  isinffi  9983  ac5num  10027  numacn  10040  acndom  10042  acndom2  10045  fodomacn  10047  infpss  10208  ssfin4  10301  domfin4  10302  enfin2i  10312  fin23lem31  10334  fin23lem41  10343  axcclem  10448  canthp1lem1  10643  canthp1  10645  winafp  10688  wun0  10709  prlem936  11038  supmul  12182  supxrre  13302  infxrre  13311  ixxub  13341  ixxlb  13342  hash1elsn  14327  relexpindlem  15006  isumltss  15790  eulerth  16712  ramub2  16943  mrieqv2d  17579  mreexexlem4d  17587  acsinfd  18505  acsdomd  18506  dfgrp3lem  18917  issubg2  19015  psgnunilem3  19358  sylow1lem4  19463  sylow3  19495  prmcyg  19756  ablfaclem3  19951  lbspss  20685  lsmcv  20746  cygzn  21117  lbslcic  21387  lmff  22796  tgcmp  22896  hauscmplem  22901  clsconn  22925  2ndcsep  22954  1stcelcls  22956  ptcnplem  23116  txcn  23121  fbdmn0  23329  ptcmplem2  23548  ptcmplem3  23549  tsmsxplem1  23648  met2ndci  24022  nmoid  24250  phtpcer  24502  phtpcco2  24506  cmetcau  24797  iscmet3lem2  24800  bcthlem4  24835  bcthlem5  24836  ovolicc2lem2  25026  vitali  25121  mbfimaopnlem  25163  limciun  25402  vieta1lem2  25815  tgldim0eq  27743  hpgerlem  28005  cusgrfi  28704  fusgrmaxsize  28710  minvecolem5  30121  foresf1o  31729  unidifsnel  31759  unidifsnne  31760  2ndimaxp  31859  aciunf1lem  31874  fsumiunle  32022  cycpmconjslem2  32301  cycpmconjs  32302  elrspunidl  32534  qsdrng  32599  dimcl  32676  lmimdim  32677  lvecdim0i  32678  lvecdim0  32679  lssdimle  32680  dimpropd  32681  dimkerim  32700  fedgmul  32704  extdg1id  32730  locfinref  32809  esumcst  33049  esumiun  33080  unelldsys  33144  sigapildsys  33148  carsggect  33305  carsgclctunlem3  33307  erdsze2lem1  34182  erdsze2  34184  ptpconn  34212  cvmliftpht  34297  filnetlem3  35253  exlimimd  36212  poimirlem32  36508  mblfinlem2  36514  mblfinlem3  36515  mblfinlem4  36516  sdclem1  36599  sstotbnd  36631  prdsbnd  36649  prdstotbnd  36650  heibor1lem  36665  bfp  36680  eqvrelref  37468  llnn0  38375  lplnn0N  38406  lvoln0N  38450  diaglbN  39914  diaintclN  39917  dibglbN  40025  dibintclN  40026  dihglblem2aN  40152  dihintcl  40203  dvh1dim  40301  sticksstones20  40970  eldioph2lem1  41483  eldioph2lem2  41484  rencldnfilem  41543  kelac1  41790  hbt  41857  cpcoll2d  43003  cncmpmax  43701  lptre2pt  44342  itgsubsticclem  44677  stoweidlem28  44730  stoweidlem31  44733  stoweidlem46  44748  stoweidlem53  44755  stoweidlem59  44761  uniimaelsetpreimafv  46050  setrec1  47689