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

Theorem rexlimddv 2951
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 2948 . 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 1758   E.wrex 2800
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-12 1794
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1588  df-nf 1591  df-ral 2804  df-rex 2805
This theorem is referenced by:  grprinvlem  6412  grpridd  6414  oaabs2  7195  oemapvali  8004  cantnflem4  8012  cantnflem4OLD  8034  r1pwss  8103  infxpenc2lem1  8297  pwfseqlem3  8939  prlem934  9314  ltexprlem7  9323  reclem3pr  9330  00id  9656  mul02lem1  9657  addid2  9664  addcan  9665  addcan2  9666  negeu  9712  mulcand  10081  suprzcl  10833  uzwo3  11060  expmulnbnd  12114  limsupgre  13078  rlimclim1  13142  fsumcvg3  13325  oexpneg  13714  bitsfi  13752  vdwlem10  14170  mreexexlem4d  14705  mreexdomd  14707  isacs3lem  15456  grprcan  15691  sylow1  16224  pgpfi  16226  slwhash  16245  pj1id  16318  efgsfo  16358  efgredlemc  16364  dmdprdsplitlem  16657  dmdprdsplitlemOLD  16658  dpjidcl  16680  dpjidclOLD  16687  pgpfac1lem4  16702  pgpfaclem2  16706  pgpfaclem3  16707  gsummgp0  16823  lspsolv  17348  restbas  18895  restcls  18918  restntr  18919  cnpnei  19001  cnpco  19004  pnrmopn  19080  1stcfb  19182  1stcrest  19190  2ndcctbss  19192  2ndcomap  19195  dis2ndc  19197  llyidm  19225  nllyidm  19226  hausllycmp  19231  lly1stc  19233  llycmpkgen2  19256  1stckgenlem  19259  basqtop  19417  regr1lem  19445  kqreglem1  19447  kqreglem2  19448  kqnrmlem1  19449  kqnrmlem2  19450  reghmph  19499  nrmhmph  19500  qtophmeo  19523  trfbas2  19549  fbasfip  19574  fbasrn  19590  trfg  19597  ssufl  19624  fmufil  19665  ufldom  19668  uffclsflim  19737  cnpfcfi  19746  alexsublem  19749  alexsubALTlem4  19755  ptcmplem3  19759  ptcmplem4  19760  tsmsxp  19862  met1stc  20229  met2ndci  20230  prdsxmslem2  20237  metcnpi3  20254  icccmplem1  20532  xrge0tsms  20544  metdseq0  20563  cnllycmp  20661  bndth  20663  lebnumlem1  20666  lebnum  20669  cfilfcls  20918  lmle  20945  relcmpcmet  20960  pjthlem2  21058  ovolscalem2  21130  ovolicc2lem4  21136  ovolicc2lem5  21137  ioombl1  21177  uniioombllem6  21202  uniioombl  21203  opnmbllem  21215  volivth  21221  mbfinf  21277  mbfi1fseqlem6  21332  itg2cnlem1  21373  itg2cn  21375  lhop2  21621  dvcnvre  21625  aareccl  21926  aaliou3lem8  21945  aaliou3lem9  21950  ulmdvlem3  22001  mtestbdd  22004  iblulm  22006  radcnvlem1  22012  abelthlem5  22034  abelthlem8  22038  chordthm  22366  dcubic  22375  fta  22551  dchrptlem2  22738  sumdchr2  22743  2sqlem11  22848  dchrisum  22875  dchrisum0flb  22893  pntibndlem3  22975  pntlemi  22987  pjspansn  25133  chscllem3  25195  xmulcand  26242  xrge0tsmsd  26399  esumpcvgval  26673  lgambdd  27168  lgamucov  27169  lgamcvglem  27171  lgamcvg2  27186  cnpcon  27264  pconcon  27265  conpcon  27269  pconpi1  27271  cnllyscon  27279  cvmcov2  27309  cvmliftpht  27352  sinccvg  27463  btwnconn1lem13  28275  opnmbllem0  28576  mblfinlem2  28578  mblfinlem4  28580  neibastop2lem  28730  tailfb  28747  prdsbnd2  28843  cntotbnd  28844  heiborlem8  28866  heiborlem9  28867  acongrep  29472  jm2.27b  29504  lmhmfgsplit  29588  hbt  29635  cncmpmax  29903  stoweidlem62  30006  cvlcvr1  33323  llnmlplnN  33522  cdlemb  33777  paddasslem10  33812  trlcnv  34148  trlator0  34154  trlid0  34159  trlnidatb  34160  cdlemd4  34184  cdlemg5  34588  trlco  34710  cdlemj3  34806  tendo0mul  34809  tendo0mulr  34810  tendoconid  34812  erngdv  34976  erngdv-rN  34984  dihmeetlem1N  35274  dihatlat  35318  hgmaprnlem5N  35887
  Copyright terms: Public domain W3C validator