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

Theorem exlimddv 1697
Description: Existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
exlimddv.1  |-  ( ph  ->  E. x ps )
exlimddv.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
exlimddv  |-  ( ph  ->  ch )
Distinct variable groups:    ch, x    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem exlimddv
StepHypRef Expression
1 exlimddv.1 . 2  |-  ( ph  ->  E. x ps )
2 exlimddv.2 . . . 4  |-  ( (
ph  /\  ps )  ->  ch )
32ex 434 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
43exlimdv 1695 . 2  |-  ( ph  ->  ( E. x ps 
->  ch ) )
51, 4mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369   E.wex 1591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1592
This theorem is referenced by:  fvmptdv2  5784  tfrlem9a  6841  erref  7117  domdifsn  7390  xpdom2  7402  enfixsn  7416  domunsn  7457  mapdom1  7472  sucdom2  7503  fineqvlem  7523  fissuni  7612  fipreima  7613  indexfi  7615  brwdom2  7784  wdomtr  7786  unwdomg  7795  unxpwdom  7800  infdifsn  7858  isinffi  8158  ac5num  8202  numacn  8215  acndom  8217  acndom2  8220  fodomacn  8222  infpss  8382  ssfin4  8475  domfin4  8476  enfin2i  8486  fin23lem31  8508  fin23lem41  8517  axcclem  8622  canthp1lem1  8815  canthp1  8817  winafp  8860  wun0  8881  prlem936  9212  supmul  10294  supxrre  11286  infmxrre  11294  ixxub  11317  ixxlb  11318  isumltss  13307  eulerth  13854  ramub2  14071  mrieqv2d  14573  mreexexlem4d  14581  acsinfd  15346  acsdomd  15347  issubg2  15689  psgnunilem3  15995  sylow1lem4  16093  sylow3  16125  prmcyg  16363  ablfaclem3  16578  lbspss  17141  lsmcv  17200  cygzn  17962  lbslcic  18229  lmff  18864  tgcmp  18963  hauscmplem  18968  clscon  18993  2ndcsep  19022  1stcelcls  19024  ptcnplem  19153  txcn  19158  fbdmn0  19366  ptcmplem2  19584  ptcmplem3  19585  tsmsxplem1  19686  met2ndci  20056  nmoid  20280  phtpcer  20526  phtpcco2  20530  cmetcau  20759  iscmet3lem2  20762  bcthlem4  20797  bcthlem5  20798  ovolicc2lem2  20960  vitali  21052  mbfimaopnlem  21092  limciun  21328  vieta1lem2  21736  cusgrafi  23325  usgramaxsize  23330  isgrp2d  23657  minvecolem5  24217  esumcst  26450  erdsze2lem1  27021  erdsze2  27023  ptpcon  27052  cvmliftpht  27137  relexpindlem  27270  mblfinlem2  28354  mblfinlem3  28355  mblfinlem4  28356  filnetlem3  28526  sdclem1  28564  sstotbnd  28599  prdsbnd  28617  prdstotbnd  28618  heibor1lem  28633  bfp  28648  eldioph2lem1  29023  eldioph2lem2  29024  rencldnfilem  29084  kelac1  29341  hbt  29411  cncmpmax  29679  stoweidlem28  29748  stoweidlem31  29751  stoweidlem46  29766  stoweidlem53  29773  stoweidlem59  29779  llnn0  32882  lplnn0N  32913  lvoln0N  32957  diaglbN  34422  diaintclN  34425  dibglbN  34533  dibintclN  34534  dihglblem2aN  34660  dihintcl  34711  dvh1dim  34809
  Copyright terms: Public domain W3C validator