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

Theorem rexlimddv 2835
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 2832 . 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 369    e. wcel 1755   E.wrex 2706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-ral 2710  df-rex 2711
This theorem is referenced by:  grprinvlem  6290  grpridd  6292  oaabs2  7072  oemapvali  7880  cantnflem4  7888  cantnflem4OLD  7910  r1pwss  7979  infxpenc2lem1  8173  pwfseqlem3  8815  prlem934  9190  ltexprlem7  9199  reclem3pr  9206  00id  9532  mul02lem1  9533  addid2  9540  addcan  9541  addcan2  9542  negeu  9588  mulcand  9957  suprzcl  10709  uzwo3  10936  expmulnbnd  11980  limsupgre  12943  rlimclim1  13007  fsumcvg3  13190  oexpneg  13578  bitsfi  13616  vdwlem10  14034  mreexexlem4d  14568  mreexdomd  14570  isacs3lem  15319  grprcan  15551  sylow1  16082  pgpfi  16084  slwhash  16103  pj1id  16176  efgsfo  16216  efgredlemc  16222  dmdprdsplitlem  16508  dmdprdsplitlemOLD  16509  dpjidcl  16531  dpjidclOLD  16538  pgpfac1lem4  16553  pgpfaclem2  16557  pgpfaclem3  16558  gsummgp0  16634  lspsolv  17146  restbas  18604  restcls  18627  restntr  18628  cnpnei  18710  cnpco  18713  pnrmopn  18789  1stcfb  18891  1stcrest  18899  2ndcctbss  18901  2ndcomap  18904  dis2ndc  18906  llyidm  18934  nllyidm  18935  hausllycmp  18940  lly1stc  18942  llycmpkgen2  18965  1stckgenlem  18968  basqtop  19126  regr1lem  19154  kqreglem1  19156  kqreglem2  19157  kqnrmlem1  19158  kqnrmlem2  19159  reghmph  19208  nrmhmph  19209  qtophmeo  19232  trfbas2  19258  fbasfip  19283  fbasrn  19299  trfg  19306  ssufl  19333  fmufil  19374  ufldom  19377  uffclsflim  19446  cnpfcfi  19455  alexsublem  19458  alexsubALTlem4  19464  ptcmplem3  19468  ptcmplem4  19469  tsmsxp  19571  met1stc  19938  met2ndci  19939  prdsxmslem2  19946  metcnpi3  19963  icccmplem1  20241  xrge0tsms  20253  metdseq0  20272  cnllycmp  20370  bndth  20372  lebnumlem1  20375  lebnum  20378  cfilfcls  20627  lmle  20654  relcmpcmet  20669  pjthlem2  20767  ovolscalem2  20839  ovolicc2lem4  20845  ovolicc2lem5  20846  ioombl1  20885  uniioombllem6  20910  uniioombl  20911  opnmbllem  20923  volivth  20929  mbfinf  20985  mbfi1fseqlem6  21040  itg2cnlem1  21081  itg2cn  21083  lhop2  21329  dvcnvre  21333  aareccl  21677  aaliou3lem8  21696  aaliou3lem9  21701  ulmdvlem3  21752  mtestbdd  21755  iblulm  21757  radcnvlem1  21763  abelthlem5  21785  abelthlem8  21789  chordthm  22117  dcubic  22126  fta  22302  dchrptlem2  22489  sumdchr2  22494  2sqlem11  22599  dchrisum  22626  dchrisum0flb  22644  pntibndlem3  22726  pntlemi  22738  pjspansn  24803  chscllem3  24865  xmulcand  25919  xrge0tsmsd  26106  esumpcvgval  26381  lgambdd  26871  lgamucov  26872  lgamcvglem  26874  lgamcvg2  26889  cnpcon  26967  pconcon  26968  conpcon  26972  pconpi1  26974  cnllyscon  26982  cvmcov2  27012  cvmliftpht  27055  sinccvg  27165  btwnconn1lem13  27977  opnmbllem0  28271  mblfinlem2  28273  mblfinlem4  28275  neibastop2lem  28425  tailfb  28442  prdsbnd2  28538  cntotbnd  28539  heiborlem8  28561  heiborlem9  28562  acongrep  29168  jm2.27b  29200  lmhmfgsplit  29284  hbt  29331  cncmpmax  29599  stoweidlem62  29703  cvlcvr1  32557  llnmlplnN  32756  cdlemb  33011  paddasslem10  33046  trlcnv  33382  trlator0  33388  trlid0  33393  trlnidatb  33394  cdlemd4  33418  cdlemg5  33822  trlco  33944  cdlemj3  34040  tendo0mul  34043  tendo0mulr  34044  tendoconid  34046  erngdv  34210  erngdv-rN  34218  dihmeetlem1N  34508  dihatlat  34552  hgmaprnlem5N  35121
  Copyright terms: Public domain W3C validator