Theorem exlimddv 1970

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813

This theorem is used by:  vtocld  3526  n0limd  4304  fvmptdv2  7043  fprresex  8366  tfrlem9a  8432  erref  8776  domdifsn  9117  xpdom2  9129  enfixsn  9143  domunsn  9184  mapdom1  9199  sucdom2  9256  fineqvlem  9295  fissuni  9384  fipreima  9385  indexfi  9387  brwdom2  9604  wdomtr  9606  unwdomg  9615  unxpwdom  9620  infdifsn  9695  setrec1  10009  isinffi  10112  ac5num  10154  numacn  10167  acndom  10169  acndom2  10172  fodomacn  10174  infpss  10333  ssfin4  10427  domfin4  10428  enfin2i  10438  fin23lem31  10460  fin23lem41  10469  axcclem  10574  canthp1lem1  10776  canthp1  10778  winafp  10821  wun0  10842  prlem936  11171  supmul  12329  supxrre  13497  infxrre  13507  ixxub  13537  ixxlb  13538  hash1elsn  14556  relexpindlem  15259  isumltss  16061  eulerth  17004  ramub2  17236  mrieqv2d  17863  mreexexlem4d  17871  acsinfd  18780  acsdomd  18781  dfgrp3lem  19298  issubg2  19402  psgnunilem3  19761  sylow1lem4  19866  sylow3  19898  prmcyg  20159  ablfaclem3  20354  lbspss  21408  lsmcv  21470  ssdifidlprm  21693  cygzn  21931  lbslcic  22202  lmff  23674  tgcmp  23774  hauscmplem  23779  clsconn  23803  2ndcsep  23833  1stcelcls  23835  ptcnplem  23995  txcn  24000  fbdmn0  24208  ptcmplem2  24427  ptcmplem3  24428  tsmsxplem1  24527  met2ndci  24896  nmoid  25116  phtpcer  25371  phtpcco2  25375  cmetcau  25665  iscmet3lem2  25668  bcthlem4  25703  bcthlem5  25704  ovolicc2lem2  25894  vitali  25989  mbfimaopnlem  26031  limciun  26269  vieta1lem2  26689  tgldim0eq  29023  hpgerlem  29300  cusgrfi  30096  fusgrmaxsize  30102  minvecolem5  31540  foresf1o  33199  unidifsnel  33229  unidifsnne  33230  2ndimaxp  33338  aciunf1lem  33354  padct  33407  fsumiunle  33516  gsumwrd2dccatlem  33737  cycpmconjslem2  33815  cycpmconjs  33816  elrspunidl  34082  krullndrng  34109  qsdrng  34125  dflring3  34133  1arithidom  34173  1arithufdlem4  34183  dimcl  34346  lmimdim  34347  lmicdim  34348  lvecdim0i  34349  lvecdim0  34350  lssdimle  34351  dimpropd  34352  dimkerim  34370  fedgmul  34374  extdg1id  34409  locfinref  34584  esumcst  34806  esumiun  34837  unelldsys  34902  sigapildsys  34906  omssubadd  35043  carsggect  35061  carsgclctunlem3  35063  erdsze2lem1  36176  erdsze2  36178  ptpconn  36206  cvmliftpht  36291  filnetlem3  37383  numiunnum  37473  exlimimd  38534  poimirlem32  38838  mblfinlem2  38844  mblfinlem3  38845  mblfinlem4  38846  sdclem1  38943  sstotbnd  38975  prdsbnd  38993  prdstotbnd  38994  heibor1lem  39009  bfp  39024  eqvrelref  39892  llnn0  40839  lplnn0N  40870  lvoln0N  40914  diaglbN  42378  diaintclN  42381  dibglbN  42489  dibintclN  42490  dihglblem2aN  42616  dihintcl  42667  dvh1dim  42765  sticksstones20  43482  eldioph2lem1  44037  eldioph2lem2  44038  rencldnfilem  44093  kelac1  44331  hbt  44397  cpcoll2d  45504  fingrphf  46300  cncmpmax  46323  lptre2pt  46923  itgsubsticclem  47258  stoweidlem28  47311  stoweidlem31  47314  stoweidlem46  47329  stoweidlem53  47336  stoweidlem59  47342  tmachlem-franscan  48232  uniimaelsetpreimafv  48751  iinfssc  50502  iinfsubc  50503  imaid  50601  uobrcl  50640  uobeq2  50867  thincciso4  50923  termcbas2  50948  termchom  50954  termcterm2  50980  euendfunc  50992  termcarweu  50994  diag1f1o  51000  diag2f1o  51006  termfucterm  51013  uobeqterm  51015