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

Theorem rexlimddv 2895
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 2892 . 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 375    e. wcel 1898   E.wrex 2750
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-ral 2754  df-rex 2755
This theorem is referenced by:  grprinvlem  6539  grpridd  6541  oaabs2  7377  oemapvali  8220  cantnflem4  8228  r1pwss  8286  infxpenc2lem1  8481  pwfseqlem3  9116  prlem934  9489  ltexprlem7  9498  reclem3pr  9505  00id  9839  mul02lem1  9840  addid2  9847  addcan  9848  addcan2  9849  negeu  9896  mulcand  10278  suprzcl  11049  uzwo3  11293  expmulnbnd  12442  limsupgre  13597  limsupgreOLD  13598  rlimclim1  13664  fsumcvg3  13850  oexpneg  14423  bitsfi  14466  vdwlem10  14995  mreexexlem4d  15608  mreexdomd  15610  isacs3lem  16467  grprcan  16754  sylow1  17310  pgpfi  17312  slwhash  17331  pj1id  17404  efgsfo  17444  efgredlemc  17450  dmdprdsplitlem  17725  dpjidcl  17746  pgpfac1lem4  17766  pgpfaclem2  17770  pgpfaclem3  17771  gsummgp0  17891  lspsolv  18421  restbas  20229  restcls  20252  restntr  20253  cnpnei  20335  cnpco  20338  pnrmopn  20414  1stcfb  20515  1stcrest  20523  2ndcctbss  20525  2ndcomap  20528  dis2ndc  20530  llyidm  20558  nllyidm  20559  hausllycmp  20564  lly1stc  20566  llycmpkgen2  20620  1stckgenlem  20623  basqtop  20781  regr1lem  20809  kqreglem1  20811  kqreglem2  20812  kqnrmlem1  20813  kqnrmlem2  20814  reghmph  20863  nrmhmph  20864  qtophmeo  20887  trfbas2  20913  fbasfip  20938  fbasrn  20954  trfg  20961  ssufl  20988  fmufil  21029  ufldom  21032  uffclsflim  21101  cnpfcfi  21110  alexsublem  21114  alexsubALTlem4  21120  ptcmplem3  21124  ptcmplem4  21125  tsmsxp  21224  met1stc  21591  met2ndci  21592  prdsxmslem2  21599  metcnpi3  21616  icccmplem1  21895  xrge0tsms  21907  metdseq0  21926  metdseq0OLD  21941  cnllycmp  22039  bndth  22041  lebnumlem1  22044  lebnumlem1OLD  22047  lebnum  22050  cfilfcls  22299  lmle  22326  relcmpcmet  22341  pjthlem2  22447  ovolscalem2  22522  ovolicc2lem4OLD  22528  ovolicc2lem4  22529  ovolicc2lem5  22530  ioombl1  22571  uniioombllem6  22602  uniioombl  22603  opnmbllem  22615  volivth  22621  mbfinf  22677  mbfinfOLD  22678  mbfi1fseqlem6  22734  itg2cnlem1  22775  itg2cn  22777  lhop2  23023  dvcnvre  23027  aareccl  23338  aaliou3lem8  23357  aaliou3lem9  23362  ulmdvlem3  23413  mtestbdd  23416  iblulm  23418  radcnvlem1  23424  abelthlem5  23446  abelthlem8  23450  chordthm  23819  dcubic  23828  lgambdd  24018  lgamucov  24019  lgamcvglem  24021  lgamcvg2  24036  fta  24062  dchrptlem2  24249  sumdchr2  24254  2sqlem11  24359  dchrisum  24386  dchrisum0flb  24404  pntibndlem3  24486  pntlemi  24498  pjspansn  27286  chscllem3  27348  xmulcand  28442  xrge0tsmsd  28599  esumpcvgval  28950  cnpcon  30003  pconcon  30004  conpcon  30008  pconpi1  30010  cnllyscon  30018  cvmcov2  30048  cvmliftpht  30091  mthmpps  30270  sinccvg  30367  btwnconn1lem13  30916  neibastop2lem  31066  tailfb  31083  poimirlem29  32015  opnmbllem0  32022  mblfinlem2  32024  mblfinlem4  32026  prdsbnd2  32173  cntotbnd  32174  heiborlem8  32196  heiborlem9  32197  cvlcvr1  32951  llnmlplnN  33150  cdlemb  33405  paddasslem10  33440  trlcnv  33777  trlator0  33783  trlid0  33788  trlnidatb  33789  cdlemd4  33813  cdlemg5  34218  trlco  34340  cdlemj3  34436  tendo0mul  34439  tendo0mulr  34440  tendoconid  34442  erngdv  34606  erngdv-rN  34614  dihmeetlem1N  34904  dihatlat  34948  hgmaprnlem5N  35517  acongrep  35876  jm2.27b  35907  lmhmfgsplit  35990  hbt  36035  imo72b2lem1  36660  cncmpmax  37394  stoweidlem62  38024  stoweidlem62OLD  38025  oexpnegALTV  38941  oexpnegnz  38942  aacllem  40909
  Copyright terms: Public domain W3C validator