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

Theorem rexlimddv 2959
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 2956 . 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 1767   E.wrex 2815
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-ral 2819  df-rex 2820
This theorem is referenced by:  grprinvlem  6495  grpridd  6497  oaabs2  7291  oemapvali  8099  cantnflem4  8107  cantnflem4OLD  8129  r1pwss  8198  infxpenc2lem1  8392  pwfseqlem3  9034  prlem934  9407  ltexprlem7  9416  reclem3pr  9423  00id  9750  mul02lem1  9751  addid2  9758  addcan  9759  addcan2  9760  negeu  9806  mulcand  10178  suprzcl  10936  uzwo3  11173  expmulnbnd  12262  limsupgre  13263  rlimclim1  13327  fsumcvg3  13510  oexpneg  13904  bitsfi  13942  vdwlem10  14363  mreexexlem4d  14898  mreexdomd  14900  isacs3lem  15649  grprcan  15884  sylow1  16419  pgpfi  16421  slwhash  16440  pj1id  16513  efgsfo  16553  efgredlemc  16559  dmdprdsplitlem  16874  dmdprdsplitlemOLD  16875  dpjidcl  16897  dpjidclOLD  16904  pgpfac1lem4  16919  pgpfaclem2  16923  pgpfaclem3  16924  gsummgp0  17040  lspsolv  17572  restbas  19425  restcls  19448  restntr  19449  cnpnei  19531  cnpco  19534  pnrmopn  19610  1stcfb  19712  1stcrest  19720  2ndcctbss  19722  2ndcomap  19725  dis2ndc  19727  llyidm  19755  nllyidm  19756  hausllycmp  19761  lly1stc  19763  llycmpkgen2  19786  1stckgenlem  19789  basqtop  19947  regr1lem  19975  kqreglem1  19977  kqreglem2  19978  kqnrmlem1  19979  kqnrmlem2  19980  reghmph  20029  nrmhmph  20030  qtophmeo  20053  trfbas2  20079  fbasfip  20104  fbasrn  20120  trfg  20127  ssufl  20154  fmufil  20195  ufldom  20198  uffclsflim  20267  cnpfcfi  20276  alexsublem  20279  alexsubALTlem4  20285  ptcmplem3  20289  ptcmplem4  20290  tsmsxp  20392  met1stc  20759  met2ndci  20760  prdsxmslem2  20767  metcnpi3  20784  icccmplem1  21062  xrge0tsms  21074  metdseq0  21093  cnllycmp  21191  bndth  21193  lebnumlem1  21196  lebnum  21199  cfilfcls  21448  lmle  21475  relcmpcmet  21490  pjthlem2  21588  ovolscalem2  21660  ovolicc2lem4  21666  ovolicc2lem5  21667  ioombl1  21707  uniioombllem6  21732  uniioombl  21733  opnmbllem  21745  volivth  21751  mbfinf  21807  mbfi1fseqlem6  21862  itg2cnlem1  21903  itg2cn  21905  lhop2  22151  dvcnvre  22155  aareccl  22456  aaliou3lem8  22475  aaliou3lem9  22480  ulmdvlem3  22531  mtestbdd  22534  iblulm  22536  radcnvlem1  22542  abelthlem5  22564  abelthlem8  22568  chordthm  22896  dcubic  22905  fta  23081  dchrptlem2  23268  sumdchr2  23273  2sqlem11  23378  dchrisum  23405  dchrisum0flb  23423  pntibndlem3  23505  pntlemi  23517  pjspansn  26171  chscllem3  26233  xmulcand  27285  xrge0tsmsd  27438  esumpcvgval  27724  lgambdd  28219  lgamucov  28220  lgamcvglem  28222  lgamcvg2  28237  cnpcon  28315  pconcon  28316  conpcon  28320  pconpi1  28322  cnllyscon  28330  cvmcov2  28360  cvmliftpht  28403  sinccvg  28514  btwnconn1lem13  29326  opnmbllem0  29627  mblfinlem2  29629  mblfinlem4  29631  neibastop2lem  29781  tailfb  29798  prdsbnd2  29894  cntotbnd  29895  heiborlem8  29917  heiborlem9  29918  acongrep  30522  jm2.27b  30552  lmhmfgsplit  30636  hbt  30683  cncmpmax  30985  stoweidlem62  31362  cvlcvr1  34136  llnmlplnN  34335  cdlemb  34590  paddasslem10  34625  trlcnv  34961  trlator0  34967  trlid0  34972  trlnidatb  34973  cdlemd4  34997  cdlemg5  35401  trlco  35523  cdlemj3  35619  tendo0mul  35622  tendo0mulr  35623  tendoconid  35625  erngdv  35789  erngdv-rN  35797  dihmeetlem1N  36087  dihatlat  36131  hgmaprnlem5N  36700
  Copyright terms: Public domain W3C validator