Theorem exlimddv 1978

Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1973). (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 403	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	exlimdv 1976	. 2 ⊢ (𝜑 → (∃𝑥𝜓 → 𝜒))
5	1, 4	mpd 15	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wi 4   ∧ wa 386  ∃wex 1823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1824

This theorem is referenced by:  fvmptdv2  6561  wfrlem17  7716  tfrlem9a  7767  erref  8048  domdifsn  8333  xpdom2  8345  enfixsn  8359  domunsn  8400  mapdom1  8415  sucdom2  8446  fineqvlem  8464  fissuni  8561  fipreima  8562  indexfi  8564  brwdom2  8769  wdomtr  8771  unwdomg  8780  unxpwdom  8785  infdifsn  8853  isinffi  9153  ac5num  9194  numacn  9207  acndom  9209  acndom2  9212  fodomacn  9214  infpss  9376  ssfin4  9469  domfin4  9470  enfin2i  9480  fin23lem31  9502  fin23lem41  9511  axcclem  9616  canthp1lem1  9811  canthp1  9813  winafp  9856  wun0  9877  prlem936  10206  supmul  11353  supxrre  12473  infxrre  12482  ixxub  12512  ixxlb  12513  relexpindlem  14214  isumltss  14988  eulerth  15896  ramub2  16126  mrieqv2d  16689  mreexexlem4d  16697  acsinfd  17570  acsdomd  17571  dfgrp3lem  17904  issubg2  17997  psgnunilem3  18304  sylow1lem4  18404  sylow3  18436  prmcyg  18685  ablfaclem3  18877  lbspss  19481  lsmcv  19541  cygzn  20318  lbslcic  20588  lmff  21517  tgcmp  21617  hauscmplem  21622  clsconn  21646  2ndcsep  21675  1stcelcls  21677  ptcnplem  21837  txcn  21842  fbdmn0  22050  ptcmplem2  22269  ptcmplem3  22270  tsmsxplem1  22368  met2ndci  22739  nmoid  22958  phtpcer  23206  phtpcco2  23210  cmetcau  23499  iscmet3lem2  23502  bcthlem4  23537  bcthlem5  23538  ovolicc2lem2  23726  vitali  23821  mbfimaopnlem  23863  limciun  24099  vieta1lem2  24507  tgldim0eq  25858  hpgerlem  26117  cusgrfi  26810  fusgrmaxsize  26816  minvecolem5  28313  foresf1o  29909  aciunf1lem  30031  fsumiunle  30143  dimcl  30427  lssdimle  30428  dimpropd  30429  dimkerim  30445  locfinref  30510  esumcst  30727  esumiun  30758  unelldsys  30823  sigapildsys  30827  carsggect  30982  carsgclctunlem3  30984  erdsze2lem1  31788  erdsze2  31790  ptpconn  31818  cvmliftpht  31903  filnetlem3  32967  exlimimd  33789  poimirlem32  34072  mblfinlem2  34078  mblfinlem3  34079  mblfinlem4  34080  sdclem1  34168  sstotbnd  34203  prdsbnd  34221  prdstotbnd  34222  heibor1lem  34237  bfp  34252  eqvrelref  34985  llnn0  35675  lplnn0N  35706  lvoln0N  35750  diaglbN  37214  diaintclN  37217  dibglbN  37325  dibintclN  37326  dihglblem2aN  37452  dihintcl  37503  dvh1dim  37601  eldioph2lem1  38293  eldioph2lem2  38294  rencldnfilem  38354  kelac1  38602  hbt  38669  cncmpmax  40134  lptre2pt  40790  itgsubsticclem  41128  stoweidlem28  41182  stoweidlem31  41185  stoweidlem46  41200  stoweidlem53  41207  stoweidlem59  41213  setrec1  43553