Theorem exlimddv 1942

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787

This theorem is referenced by:  vtocld  3509  fvmptdv2  6961  fprresex  8257  tfrlem9a  8322  erref  8661  domdifsn  8995  xpdom2  9007  enfixsn  9021  domunsn  9062  mapdom1  9077  sucdom2  9134  fineqvlem  9173  fissuni  9264  fipreima  9265  indexfi  9267  brwdom2  9485  wdomtr  9487  unwdomg  9496  unxpwdom  9501  infdifsn  9576  isinffi  9914  ac5num  9956  numacn  9969  acndom  9971  acndom2  9974  fodomacn  9976  infpss  10136  ssfin4  10230  domfin4  10231  enfin2i  10241  fin23lem31  10263  fin23lem41  10272  axcclem  10377  canthp1lem1  10573  canthp1  10575  winafp  10618  wun0  10639  prlem936  10968  supmul  12126  supxrre  13277  infxrre  13287  ixxub  13317  ixxlb  13318  hash1elsn  14331  relexpindlem  15023  isumltss  15811  eulerth  16751  ramub2  16983  mrieqv2d  17603  mreexexlem4d  17611  acsinfd  18520  acsdomd  18521  dfgrp3lem  19012  issubg2  19115  psgnunilem3  19469  sylow1lem4  19574  sylow3  19606  prmcyg  19867  ablfaclem3  20062  lbspss  21079  lsmcv  21141  cygzn  21552  lbslcic  21823  lmff  23291  tgcmp  23391  hauscmplem  23396  clsconn  23420  2ndcsep  23449  1stcelcls  23451  ptcnplem  23611  txcn  23616  fbdmn0  23824  ptcmplem2  24043  ptcmplem3  24044  tsmsxplem1  24143  met2ndci  24512  nmoid  24732  phtpcer  24987  phtpcco2  24991  cmetcau  25281  iscmet3lem2  25284  bcthlem4  25319  bcthlem5  25320  ovolicc2lem2  25510  vitali  25605  mbfimaopnlem  25647  limciun  25886  vieta1lem2  26302  tgldim0eq  28596  hpgerlem  28858  cusgrfi  29552  fusgrmaxsize  29558  minvecolem5  30977  n0limd  32566  foresf1o  32599  unidifsnel  32630  unidifsnne  32631  2ndimaxp  32745  aciunf1lem  32761  padct  32817  fsumiunle  32928  gsumwrd2dccatlem  33165  cycpmconjslem2  33243  cycpmconjs  33244  elrspunidl  33518  ssdifidlprm  33548  krullndrng  33571  qsdrng  33587  1arithidom  33627  1arithufdlem4  33637  dimcl  33794  lmimdim  33795  lmicdim  33796  lvecdim0i  33797  lvecdim0  33798  lssdimle  33799  dimpropd  33800  dimkerim  33818  fedgmul  33822  extdg1id  33857  locfinref  34032  esumcst  34254  esumiun  34285  unelldsys  34349  sigapildsys  34353  carsggect  34509  carsgclctunlem3  34511  erdsze2lem1  35438  erdsze2  35440  ptpconn  35468  cvmliftpht  35553  filnetlem3  36615  numiunnum  36705  exlimimd  37712  poimirlem32  38026  mblfinlem2  38032  mblfinlem3  38033  mblfinlem4  38034  sdclem1  38117  sstotbnd  38149  prdsbnd  38167  prdstotbnd  38168  heibor1lem  38183  bfp  38198  eqvrelref  39068  llnn0  40015  lplnn0N  40046  lvoln0N  40090  diaglbN  41554  diaintclN  41557  dibglbN  41665  dibintclN  41666  dihglblem2aN  41792  dihintcl  41843  dvh1dim  41941  sticksstones20  42658  eldioph2lem1  43216  eldioph2lem2  43217  rencldnfilem  43272  kelac1  43515  hbt  43582  cpcoll2d  44710  cncmpmax  45487  lptre2pt  46090  itgsubsticclem  46425  stoweidlem28  46478  stoweidlem31  46481  stoweidlem46  46496  stoweidlem53  46503  stoweidlem59  46509  uniimaelsetpreimafv  47878  iinfssc  49554  iinfsubc  49555  imaid  49651  uobrcl  49690  uobeq2  49898  thincciso4  49954  termcbas2  49979  termchom  49985  termcterm2  50011  euendfunc  50023  termcarweu  50025  diag1f1o  50031  diag2f1o  50034  termfucterm  50041  uobeqterm  50043  setrec1  50188