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

Theorem rexlimddv 2950
Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1  |-  ( ph  ->  E. x  e.  A  ps )
rexlimddv.2  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
Assertion
Ref Expression
rexlimddv  |-  ( ph  ->  ch )
Distinct variable groups:    ph, x    ch, x
Allowed substitution hints:    ps( x)    A( x)

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2  |-  ( ph  ->  E. x  e.  A  ps )
2 rexlimddv.2 . . 3  |-  ( (
ph  /\  ( x  e.  A  /\  ps )
)  ->  ch )
32rexlimdvaa 2947 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
41, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    e. wcel 1823   E.wrex 2805
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709
This theorem depends on definitions:  df-bi 185  df-an 369  df-ex 1618  df-ral 2809  df-rex 2810
This theorem is referenced by:  grprinvlem  6486  grpridd  6488  oaabs2  7286  oemapvali  8094  cantnflem4  8102  cantnflem4OLD  8124  r1pwss  8193  infxpenc2lem1  8387  pwfseqlem3  9027  prlem934  9400  ltexprlem7  9409  reclem3pr  9416  00id  9744  mul02lem1  9745  addid2  9752  addcan  9753  addcan2  9754  negeu  9801  mulcand  10178  suprzcl  10938  uzwo3  11178  expmulnbnd  12280  limsupgre  13386  rlimclim1  13450  fsumcvg3  13633  oexpneg  14133  bitsfi  14171  vdwlem10  14592  mreexexlem4d  15136  mreexdomd  15138  isacs3lem  15995  grprcan  16282  sylow1  16822  pgpfi  16824  slwhash  16843  pj1id  16916  efgsfo  16956  efgredlemc  16962  dmdprdsplitlem  17279  dmdprdsplitlemOLD  17280  dpjidcl  17302  dpjidclOLD  17309  pgpfac1lem4  17324  pgpfaclem2  17328  pgpfaclem3  17329  gsummgp0  17451  lspsolv  17984  restbas  19826  restcls  19849  restntr  19850  cnpnei  19932  cnpco  19935  pnrmopn  20011  1stcfb  20112  1stcrest  20120  2ndcctbss  20122  2ndcomap  20125  dis2ndc  20127  llyidm  20155  nllyidm  20156  hausllycmp  20161  lly1stc  20163  llycmpkgen2  20217  1stckgenlem  20220  basqtop  20378  regr1lem  20406  kqreglem1  20408  kqreglem2  20409  kqnrmlem1  20410  kqnrmlem2  20411  reghmph  20460  nrmhmph  20461  qtophmeo  20484  trfbas2  20510  fbasfip  20535  fbasrn  20551  trfg  20558  ssufl  20585  fmufil  20626  ufldom  20629  uffclsflim  20698  cnpfcfi  20707  alexsublem  20710  alexsubALTlem4  20716  ptcmplem3  20720  ptcmplem4  20721  tsmsxp  20823  met1stc  21190  met2ndci  21191  prdsxmslem2  21198  metcnpi3  21215  icccmplem1  21493  xrge0tsms  21505  metdseq0  21524  cnllycmp  21622  bndth  21624  lebnumlem1  21627  lebnum  21630  cfilfcls  21879  lmle  21906  relcmpcmet  21921  pjthlem2  22019  ovolscalem2  22091  ovolicc2lem4  22097  ovolicc2lem5  22098  ioombl1  22138  uniioombllem6  22163  uniioombl  22164  opnmbllem  22176  volivth  22182  mbfinf  22238  mbfi1fseqlem6  22293  itg2cnlem1  22334  itg2cn  22336  lhop2  22582  dvcnvre  22586  aareccl  22888  aaliou3lem8  22907  aaliou3lem9  22912  ulmdvlem3  22963  mtestbdd  22966  iblulm  22968  radcnvlem1  22974  abelthlem5  22996  abelthlem8  23000  chordthm  23365  dcubic  23374  fta  23551  dchrptlem2  23738  sumdchr2  23743  2sqlem11  23848  dchrisum  23875  dchrisum0flb  23893  pntibndlem3  23975  pntlemi  23987  pjspansn  26693  chscllem3  26755  xmulcand  27851  xrge0tsmsd  28010  esumpcvgval  28307  lgambdd  28843  lgamucov  28844  lgamcvglem  28846  lgamcvg2  28861  cnpcon  28939  pconcon  28940  conpcon  28944  pconpi1  28946  cnllyscon  28954  cvmcov2  28984  cvmliftpht  29027  mthmpps  29206  sinccvg  29303  btwnconn1lem13  29977  opnmbllem0  30290  mblfinlem2  30292  mblfinlem4  30294  neibastop2lem  30418  tailfb  30435  prdsbnd2  30531  cntotbnd  30532  heiborlem8  30554  heiborlem9  30555  acongrep  31157  jm2.27b  31187  lmhmfgsplit  31271  hbt  31320  cncmpmax  31647  stoweidlem62  32083  oexpnegALTV  32583  oexpnegnz  32584  aacllem  33604  cvlcvr1  35461  llnmlplnN  35660  cdlemb  35915  paddasslem10  35950  trlcnv  36287  trlator0  36293  trlid0  36298  trlnidatb  36299  cdlemd4  36323  cdlemg5  36728  trlco  36850  cdlemj3  36946  tendo0mul  36949  tendo0mulr  36950  tendoconid  36952  erngdv  37116  erngdv-rN  37124  dihmeetlem1N  37414  dihatlat  37458  hgmaprnlem5N  38027  imo72b2lem1  38440
  Copyright terms: Public domain W3C validator