MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exlimddv Structured version   Visualization version   GIF version

Theorem exlimddv 1939
Description: Existential elimination rule of natural deduction (Rule C, explained in exlimiv 1934). (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
StepHypRef Expression
1 exlimddv.1 . 2 (𝜑 → ∃𝑥𝜓)
2 exlimddv.2 . . . 4 ((𝜑𝜓) → 𝜒)
32ex 414 . . 3 (𝜑 → (𝜓𝜒))
43exlimdv 1937 . 2 (𝜑 → (∃𝑥𝜓𝜒))
51, 4mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914
This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783
This theorem is referenced by:  vtocld  3514  fvmptdv2  6971  fprresex  8246  wfrlem17OLD  8276  tfrlem9a  8337  erref  8675  domdifsn  9005  xpdom2  9018  enfixsn  9032  sucdom2OLD  9033  domunsn  9078  mapdom1  9093  sucdom2  9157  fineqvlem  9213  fissuni  9308  fipreima  9309  indexfi  9311  brwdom2  9516  wdomtr  9518  unwdomg  9527  unxpwdom  9532  infdifsn  9600  isinffi  9935  ac5num  9979  numacn  9992  acndom  9994  acndom2  9997  fodomacn  9999  infpss  10160  ssfin4  10253  domfin4  10254  enfin2i  10264  fin23lem31  10286  fin23lem41  10295  axcclem  10400  canthp1lem1  10595  canthp1  10597  winafp  10640  wun0  10661  prlem936  10990  supmul  12134  supxrre  13253  infxrre  13262  ixxub  13292  ixxlb  13293  hash1elsn  14278  relexpindlem  14955  isumltss  15740  eulerth  16662  ramub2  16893  mrieqv2d  17526  mreexexlem4d  17534  acsinfd  18452  acsdomd  18453  dfgrp3lem  18852  issubg2  18950  psgnunilem3  19285  sylow1lem4  19390  sylow3  19422  prmcyg  19678  ablfaclem3  19873  lbspss  20559  lsmcv  20618  cygzn  20993  lbslcic  21263  lmff  22668  tgcmp  22768  hauscmplem  22773  clsconn  22797  2ndcsep  22826  1stcelcls  22828  ptcnplem  22988  txcn  22993  fbdmn0  23201  ptcmplem2  23420  ptcmplem3  23421  tsmsxplem1  23520  met2ndci  23894  nmoid  24122  phtpcer  24374  phtpcco2  24378  cmetcau  24669  iscmet3lem2  24672  bcthlem4  24707  bcthlem5  24708  ovolicc2lem2  24898  vitali  24993  mbfimaopnlem  25035  limciun  25274  vieta1lem2  25687  tgldim0eq  27487  hpgerlem  27749  cusgrfi  28448  fusgrmaxsize  28454  minvecolem5  29865  foresf1o  31473  unidifsnel  31504  unidifsnne  31505  2ndimaxp  31605  aciunf1lem  31620  fsumiunle  31767  cycpmconjslem2  32046  cycpmconjs  32047  elrspunidl  32243  dimcl  32342  lvecdim0i  32343  lvecdim0  32344  lssdimle  32345  dimpropd  32346  dimkerim  32362  fedgmul  32366  extdg1id  32392  locfinref  32462  esumcst  32702  esumiun  32733  unelldsys  32797  sigapildsys  32801  carsggect  32958  carsgclctunlem3  32960  erdsze2lem1  33837  erdsze2  33839  ptpconn  33867  cvmliftpht  33952  filnetlem3  34881  exlimimd  35843  poimirlem32  36139  mblfinlem2  36145  mblfinlem3  36146  mblfinlem4  36147  sdclem1  36231  sstotbnd  36263  prdsbnd  36281  prdstotbnd  36282  heibor1lem  36297  bfp  36312  eqvrelref  37101  llnn0  38008  lplnn0N  38039  lvoln0N  38083  diaglbN  39547  diaintclN  39550  dibglbN  39658  dibintclN  39659  dihglblem2aN  39785  dihintcl  39836  dvh1dim  39934  sticksstones20  40603  eldioph2lem1  41112  eldioph2lem2  41113  rencldnfilem  41172  kelac1  41419  hbt  41486  cpcoll2d  42613  cncmpmax  43311  lptre2pt  43955  itgsubsticclem  44290  stoweidlem28  44343  stoweidlem31  44346  stoweidlem46  44361  stoweidlem53  44368  stoweidlem59  44374  uniimaelsetpreimafv  45662  setrec1  47210
  Copyright terms: Public domain W3C validator