Theorem exlimddv 1935

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

Syntax hints:   → wi 4   ∧ wa 395  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780

This theorem is referenced by:  vtocld  3527  fvmptdv2  6986  fprresex  8289  tfrlem9a  8354  erref  8691  domdifsn  9024  xpdom2  9036  enfixsn  9050  domunsn  9091  mapdom1  9106  sucdom2  9167  fineqvlem  9209  fissuni  9308  fipreima  9309  indexfi  9311  brwdom2  9526  wdomtr  9528  unwdomg  9537  unxpwdom  9542  infdifsn  9610  isinffi  9945  ac5num  9989  numacn  10002  acndom  10004  acndom2  10007  fodomacn  10009  infpss  10169  ssfin4  10263  domfin4  10264  enfin2i  10274  fin23lem31  10296  fin23lem41  10305  axcclem  10410  canthp1lem1  10605  canthp1  10607  winafp  10650  wun0  10671  prlem936  11000  supmul  12155  supxrre  13287  infxrre  13297  ixxub  13327  ixxlb  13328  hash1elsn  14336  relexpindlem  15029  isumltss  15814  eulerth  16753  ramub2  16985  mrieqv2d  17600  mreexexlem4d  17608  acsinfd  18515  acsdomd  18516  dfgrp3lem  18970  issubg2  19073  psgnunilem3  19426  sylow1lem4  19531  sylow3  19563  prmcyg  19824  ablfaclem3  20019  lbspss  20989  lsmcv  21051  cygzn  21480  lbslcic  21750  lmff  23188  tgcmp  23288  hauscmplem  23293  clsconn  23317  2ndcsep  23346  1stcelcls  23348  ptcnplem  23508  txcn  23513  fbdmn0  23721  ptcmplem2  23940  ptcmplem3  23941  tsmsxplem1  24040  met2ndci  24410  nmoid  24630  phtpcer  24894  phtpcco2  24899  cmetcau  25189  iscmet3lem2  25192  bcthlem4  25227  bcthlem5  25228  ovolicc2lem2  25419  vitali  25514  mbfimaopnlem  25556  limciun  25795  vieta1lem2  26219  tgldim0eq  28430  hpgerlem  28692  cusgrfi  29386  fusgrmaxsize  29392  minvecolem5  30810  n0limd  32401  foresf1o  32433  unidifsnel  32464  unidifsnne  32465  2ndimaxp  32570  aciunf1lem  32586  fsumiunle  32754  gsumwrd2dccatlem  33006  cycpmconjslem2  33112  cycpmconjs  33113  elrspunidl  33399  ssdifidlprm  33429  krullndrng  33452  qsdrng  33468  1arithidom  33508  1arithufdlem4  33518  dimcl  33598  lmimdim  33599  lmicdim  33600  lvecdim0i  33601  lvecdim0  33602  lssdimle  33603  dimpropd  33604  dimkerim  33623  fedgmul  33627  extdg1id  33661  locfinref  33831  esumcst  34053  esumiun  34084  unelldsys  34148  sigapildsys  34152  carsggect  34309  carsgclctunlem3  34311  erdsze2lem1  35190  erdsze2  35192  ptpconn  35220  cvmliftpht  35305  filnetlem3  36368  numiunnum  36458  exlimimd  37331  poimirlem32  37646  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  sdclem1  37737  sstotbnd  37769  prdsbnd  37787  prdstotbnd  37788  heibor1lem  37803  bfp  37818  eqvrelref  38601  llnn0  39510  lplnn0N  39541  lvoln0N  39585  diaglbN  41049  diaintclN  41052  dibglbN  41160  dibintclN  41161  dihglblem2aN  41287  dihintcl  41338  dvh1dim  41436  sticksstones20  42154  eldioph2lem1  42748  eldioph2lem2  42749  rencldnfilem  42808  kelac1  43052  hbt  43119  cpcoll2d  44248  cncmpmax  45026  lptre2pt  45638  itgsubsticclem  45973  stoweidlem28  46026  stoweidlem31  46029  stoweidlem46  46044  stoweidlem53  46051  stoweidlem59  46057  uniimaelsetpreimafv  47397  iinfssc  49046  iinfsubc  49047  imaid  49143  uobrcl  49182  uobeq2  49390  thincciso4  49446  termcbas2  49471  termchom  49477  termcterm2  49503  euendfunc  49515  termcarweu  49517  diag1f1o  49523  diag2f1o  49526  termfucterm  49533  uobeqterm  49535  setrec1  49680