Theorem exlimddv 1965

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

Syntax hints:   → wi 4   ∧ wa 400  ∃wex 1809

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

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810

This theorem is referenced by:  vtocld  3528  n0limd  4309  fvmptdv2  7010  fprresex  8308  tfrlem9a  8374  erref  8716  domdifsn  9049  xpdom2  9061  enfixsn  9075  domunsn  9116  mapdom1  9131  sucdom2  9188  fineqvlem  9227  fissuni  9315  fipreima  9316  indexfi  9318  brwdom2  9536  wdomtr  9538  unwdomg  9547  unxpwdom  9552  infdifsn  9627  isinffi  9979  ac5num  10021  numacn  10034  acndom  10036  acndom2  10039  fodomacn  10041  infpss  10200  ssfin4  10295  domfin4  10296  enfin2i  10306  fin23lem31  10328  fin23lem41  10337  axcclem  10442  canthp1lem1  10638  canthp1  10640  winafp  10683  wun0  10704  prlem936  11033  supmul  12188  supxrre  13354  infxrre  13364  ixxub  13394  ixxlb  13395  hash1elsn  14409  relexpindlem  15102  isumltss  15904  eulerth  16843  ramub2  17075  mrieqv2d  17696  mreexexlem4d  17704  acsinfd  18613  acsdomd  18614  dfgrp3lem  19105  issubg2  19209  psgnunilem3  19567  sylow1lem4  19672  sylow3  19704  prmcyg  19965  ablfaclem3  20160  lbspss  21184  lsmcv  21246  ssdifidlprm  21467  cygzn  21701  lbslcic  21972  lmff  23439  tgcmp  23539  hauscmplem  23544  clsconn  23568  2ndcsep  23597  1stcelcls  23599  ptcnplem  23759  txcn  23764  fbdmn0  23972  ptcmplem2  24191  ptcmplem3  24192  tsmsxplem1  24291  met2ndci  24660  nmoid  24880  phtpcer  25135  phtpcco2  25139  cmetcau  25429  iscmet3lem2  25432  bcthlem4  25467  bcthlem5  25468  ovolicc2lem2  25658  vitali  25753  mbfimaopnlem  25795  limciun  26034  vieta1lem2  26453  tgldim0eq  28753  hpgerlem  29028  cusgrfi  29789  fusgrmaxsize  29795  minvecolem5  31214  foresf1o  32831  unidifsnel  32862  unidifsnne  32863  2ndimaxp  32972  aciunf1lem  32988  padct  33044  fsumiunle  33154  gsumwrd2dccatlem  33378  cycpmconjslem2  33456  cycpmconjs  33457  elrspunidl  33717  krullndrng  33744  qsdrng  33760  dflring3  33768  1arithidom  33808  1arithufdlem4  33818  dimcl  33974  lmimdim  33975  lmicdim  33976  lvecdim0i  33977  lvecdim0  33978  lssdimle  33979  dimpropd  33980  dimkerim  33998  fedgmul  34002  extdg1id  34037  locfinref  34212  esumcst  34434  esumiun  34465  unelldsys  34529  sigapildsys  34533  carsggect  34689  carsgclctunlem3  34691  erdsze2lem1  35676  erdsze2  35678  ptpconn  35706  cvmliftpht  35791  filnetlem3  36872  numiunnum  36962  exlimimd  37970  poimirlem32  38284  mblfinlem2  38290  mblfinlem3  38291  mblfinlem4  38292  sdclem1  38375  sstotbnd  38407  prdsbnd  38425  prdstotbnd  38426  heibor1lem  38441  bfp  38456  eqvrelref  39324  llnn0  40271  lplnn0N  40302  lvoln0N  40346  diaglbN  41810  diaintclN  41813  dibglbN  41921  dibintclN  41922  dihglblem2aN  42048  dihintcl  42099  dvh1dim  42197  sticksstones20  42914  eldioph2lem1  43474  eldioph2lem2  43475  rencldnfilem  43530  kelac1  43773  hbt  43840  cpcoll2d  44952  cncmpmax  45735  lptre2pt  46337  itgsubsticclem  46672  stoweidlem28  46725  stoweidlem31  46728  stoweidlem46  46743  stoweidlem53  46750  stoweidlem59  46756  uniimaelsetpreimafv  48128  iinfssc  49818  iinfsubc  49819  imaid  49915  uobrcl  49954  uobeq2  50162  thincciso4  50218  termcbas2  50243  termchom  50249  termcterm2  50275  euendfunc  50287  termcarweu  50289  diag1f1o  50295  diag2f1o  50298  termfucterm  50305  uobeqterm  50307  setrec1  50452