Theorem exlimddv 1932

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

Syntax hints:   → wi 4   ∧ wa 398  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777

This theorem is referenced by:  fvmptdv2  6780  wfrlem17  7965  tfrlem9a  8016  erref  8303  domdifsn  8594  xpdom2  8606  enfixsn  8620  domunsn  8661  mapdom1  8676  sucdom2  8708  fineqvlem  8726  fissuni  8823  fipreima  8824  indexfi  8826  brwdom2  9031  wdomtr  9033  unwdomg  9042  unxpwdom  9047  infdifsn  9114  isinffi  9415  ac5num  9456  numacn  9469  acndom  9471  acndom2  9474  fodomacn  9476  infpss  9633  ssfin4  9726  domfin4  9727  enfin2i  9737  fin23lem31  9759  fin23lem41  9768  axcclem  9873  canthp1lem1  10068  canthp1  10070  winafp  10113  wun0  10134  prlem936  10463  supmul  11607  supxrre  12714  infxrre  12723  ixxub  12753  ixxlb  12754  hash1elsn  13726  relexpindlem  14416  isumltss  15197  eulerth  16114  ramub2  16344  mrieqv2d  16904  mreexexlem4d  16912  acsinfd  17784  acsdomd  17785  dfgrp3lem  18191  issubg2  18288  psgnunilem3  18618  sylow1lem4  18720  sylow3  18752  prmcyg  19008  ablfaclem3  19203  lbspss  19848  lsmcv  19907  cygzn  20711  lbslcic  20979  lmff  21903  tgcmp  22003  hauscmplem  22008  clsconn  22032  2ndcsep  22061  1stcelcls  22063  ptcnplem  22223  txcn  22228  fbdmn0  22436  ptcmplem2  22655  ptcmplem3  22656  tsmsxplem1  22755  met2ndci  23126  nmoid  23345  phtpcer  23593  phtpcco2  23597  cmetcau  23886  iscmet3lem2  23889  bcthlem4  23924  bcthlem5  23925  ovolicc2lem2  24113  vitali  24208  mbfimaopnlem  24250  limciun  24486  vieta1lem2  24894  tgldim0eq  26283  hpgerlem  26545  cusgrfi  27234  fusgrmaxsize  27240  minvecolem5  28652  foresf1o  30259  unidifsnel  30289  unidifsnne  30290  aciunf1lem  30401  fsumiunle  30540  cycpmconjslem2  30792  cycpmconjs  30793  dimcl  30998  lvecdim0i  30999  lvecdim0  31000  lssdimle  31001  dimpropd  31002  dimkerim  31018  fedgmul  31022  extdg1id  31048  locfinref  31100  esumcst  31317  esumiun  31348  unelldsys  31412  sigapildsys  31416  carsggect  31571  carsgclctunlem3  31573  erdsze2lem1  32445  erdsze2  32447  ptpconn  32475  cvmliftpht  32560  filnetlem3  33723  exlimimd  34618  poimirlem32  34918  mblfinlem2  34924  mblfinlem3  34925  mblfinlem4  34926  sdclem1  35012  sstotbnd  35047  prdsbnd  35065  prdstotbnd  35066  heibor1lem  35081  bfp  35096  eqvrelref  35839  llnn0  36646  lplnn0N  36677  lvoln0N  36721  diaglbN  38185  diaintclN  38188  dibglbN  38296  dibintclN  38297  dihglblem2aN  38423  dihintcl  38474  dvh1dim  38572  eldioph2lem1  39350  eldioph2lem2  39351  rencldnfilem  39410  kelac1  39656  hbt  39723  cpcoll2d  40588  cncmpmax  41282  lptre2pt  41914  itgsubsticclem  42253  stoweidlem28  42307  stoweidlem31  42310  stoweidlem46  42325  stoweidlem53  42332  stoweidlem59  42338  uniimaelsetpreimafv  43550  setrec1  44788