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

Theorem rexlimddv 2794
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 2791 . 2  |-  ( ph  ->  ( E. x  e.  A  ps  ->  ch ) )
41, 3mpd 15 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1721   E.wrex 2667
This theorem is referenced by:  grprinvlem  6244  grpridd  6246  oaabs2  6847  oemapvali  7596  cantnflem4  7604  r1pwss  7666  infxpenc2lem1  7856  pwfseqlem3  8491  prlem934  8866  ltexprlem7  8875  reclem3pr  8882  00id  9197  mul02lem1  9198  addid2  9205  addcan  9206  addcan2  9207  negeu  9252  mulcand  9611  suprzcl  10305  uzwo3  10525  expmulnbnd  11466  limsupgre  12230  rlimclim1  12294  fsumcvg3  12478  oexpneg  12866  bitsfi  12904  vdwlem10  13313  mreexexlem4d  13827  mreexdomd  13829  isacs3lem  14547  grprcan  14793  sylow1  15192  pgpfi  15194  slwhash  15213  pj1id  15286  efgsfo  15326  efgredlemc  15332  dmdprdsplitlem  15550  dpjidcl  15571  pgpfac1lem4  15591  pgpfaclem2  15595  pgpfaclem3  15596  lspsolv  16170  restbas  17176  restcls  17199  restntr  17200  cnpnei  17282  cnpco  17285  pnrmopn  17361  1stcfb  17461  1stcrest  17469  2ndcctbss  17471  2ndcomap  17474  dis2ndc  17476  llyidm  17504  nllyidm  17505  hausllycmp  17510  lly1stc  17512  llycmpkgen2  17535  1stckgenlem  17538  basqtop  17696  regr1lem  17724  kqreglem1  17726  kqreglem2  17727  kqnrmlem1  17728  kqnrmlem2  17729  reghmph  17778  nrmhmph  17779  qtophmeo  17802  trfbas2  17828  fbasfip  17853  fbasrn  17869  trfg  17876  ssufl  17903  fmufil  17944  ufldom  17947  uffclsflim  18016  cnpfcfi  18025  alexsublem  18028  alexsubALTlem4  18034  ptcmplem3  18038  ptcmplem4  18039  tsmsxp  18137  met1stc  18504  met2ndci  18505  prdsxmslem2  18512  metcnpi3  18529  icccmplem1  18806  xrge0tsms  18818  metdseq0  18837  cnllycmp  18934  bndth  18936  lebnumlem1  18939  lebnum  18942  cfilfcls  19180  lmle  19207  relcmpcmet  19222  pjthlem2  19292  ovolscalem2  19363  ovolicc2lem4  19369  ovolicc2lem5  19370  ioombl1  19409  uniioombllem6  19433  uniioombl  19434  opnmbllem  19446  volivth  19452  mbfinf  19510  mbfi1fseqlem6  19565  itg2cnlem1  19606  itg2cn  19608  lhop2  19852  dvcnvre  19856  aareccl  20196  aaliou3lem8  20215  aaliou3lem9  20220  ulmdvlem3  20271  mtestbdd  20274  iblulm  20276  radcnvlem1  20282  abelthlem5  20304  abelthlem8  20308  chordthm  20631  dcubic  20639  fta  20815  dchrptlem2  21002  sumdchr2  21007  2sqlem11  21112  dchrisum  21139  dchrisum0flb  21157  pntibndlem3  21239  pntlemi  21251  pjspansn  23032  chscllem3  23094  xmulcand  24120  xrge0tsmsd  24176  esumpcvgval  24421  lgambdd  24774  lgamucov  24775  lgamcvglem  24777  lgamcvg2  24792  cnpcon  24870  pconcon  24871  conpcon  24875  pconpi1  24877  cnllyscon  24885  cvmcov2  24915  cvmliftpht  24958  sinccvg  25063  btwnconn1lem13  25937  mblfinlem  26143  mblfinlem3  26145  neibastop2lem  26279  tailfb  26296  prdsbnd2  26394  cntotbnd  26395  heiborlem8  26417  heiborlem9  26418  acongrep  26935  jm2.27b  26967  lmhmfgsplit  27052  hbt  27202  cncmpmax  27570  stoweidlem62  27678  cvlcvr1  29822  llnmlplnN  30021  cdlemb  30276  paddasslem10  30311  trlcnv  30647  trlator0  30653  trlid0  30658  trlnidatb  30659  cdlemd4  30683  cdlemg5  31087  trlco  31209  cdlemj3  31305  tendo0mul  31308  tendo0mulr  31309  tendoconid  31311  erngdv  31475  erngdv-rN  31483  dihmeetlem1N  31773  dihatlat  31817  hgmaprnlem5N  32386
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-nf 1551  df-ral 2671  df-rex 2672
  Copyright terms: Public domain W3C validator