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

Theorem rexlimddv 2939
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 2936 . 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 1804   E.wrex 2794
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1600  df-ral 2798  df-rex 2799
This theorem is referenced by:  grprinvlem  6498  grpridd  6500  oaabs2  7296  oemapvali  8106  cantnflem4  8114  cantnflem4OLD  8136  r1pwss  8205  infxpenc2lem1  8399  pwfseqlem3  9041  prlem934  9414  ltexprlem7  9423  reclem3pr  9430  00id  9758  mul02lem1  9759  addid2  9766  addcan  9767  addcan2  9768  negeu  9815  mulcand  10188  suprzcl  10948  uzwo3  11186  expmulnbnd  12277  limsupgre  13283  rlimclim1  13347  fsumcvg3  13530  oexpneg  13926  bitsfi  13964  vdwlem10  14385  mreexexlem4d  14921  mreexdomd  14923  isacs3lem  15670  grprcan  15957  sylow1  16497  pgpfi  16499  slwhash  16518  pj1id  16591  efgsfo  16631  efgredlemc  16637  dmdprdsplitlem  16958  dmdprdsplitlemOLD  16959  dpjidcl  16981  dpjidclOLD  16988  pgpfac1lem4  17003  pgpfaclem2  17007  pgpfaclem3  17008  gsummgp0  17130  lspsolv  17663  restbas  19532  restcls  19555  restntr  19556  cnpnei  19638  cnpco  19641  pnrmopn  19717  1stcfb  19819  1stcrest  19827  2ndcctbss  19829  2ndcomap  19832  dis2ndc  19834  llyidm  19862  nllyidm  19863  hausllycmp  19868  lly1stc  19870  llycmpkgen2  19924  1stckgenlem  19927  basqtop  20085  regr1lem  20113  kqreglem1  20115  kqreglem2  20116  kqnrmlem1  20117  kqnrmlem2  20118  reghmph  20167  nrmhmph  20168  qtophmeo  20191  trfbas2  20217  fbasfip  20242  fbasrn  20258  trfg  20265  ssufl  20292  fmufil  20333  ufldom  20336  uffclsflim  20405  cnpfcfi  20414  alexsublem  20417  alexsubALTlem4  20423  ptcmplem3  20427  ptcmplem4  20428  tsmsxp  20530  met1stc  20897  met2ndci  20898  prdsxmslem2  20905  metcnpi3  20922  icccmplem1  21200  xrge0tsms  21212  metdseq0  21231  cnllycmp  21329  bndth  21331  lebnumlem1  21334  lebnum  21337  cfilfcls  21586  lmle  21613  relcmpcmet  21628  pjthlem2  21726  ovolscalem2  21798  ovolicc2lem4  21804  ovolicc2lem5  21805  ioombl1  21845  uniioombllem6  21870  uniioombl  21871  opnmbllem  21883  volivth  21889  mbfinf  21945  mbfi1fseqlem6  22000  itg2cnlem1  22041  itg2cn  22043  lhop2  22289  dvcnvre  22293  aareccl  22594  aaliou3lem8  22613  aaliou3lem9  22618  ulmdvlem3  22669  mtestbdd  22672  iblulm  22674  radcnvlem1  22680  abelthlem5  22702  abelthlem8  22706  chordthm  23040  dcubic  23049  fta  23225  dchrptlem2  23412  sumdchr2  23417  2sqlem11  23522  dchrisum  23549  dchrisum0flb  23567  pntibndlem3  23649  pntlemi  23661  pjspansn  26367  chscllem3  26429  xmulcand  27490  xrge0tsmsd  27648  esumpcvgval  27957  lgambdd  28452  lgamucov  28453  lgamcvglem  28455  lgamcvg2  28470  cnpcon  28548  pconcon  28549  conpcon  28553  pconpi1  28555  cnllyscon  28563  cvmcov2  28593  cvmliftpht  28636  mthmpps  28815  sinccvg  28912  btwnconn1lem13  29724  opnmbllem0  30025  mblfinlem2  30027  mblfinlem4  30029  neibastop2lem  30153  tailfb  30170  prdsbnd2  30266  cntotbnd  30267  heiborlem8  30289  heiborlem9  30290  acongrep  30893  jm2.27b  30923  lmhmfgsplit  31007  hbt  31054  cncmpmax  31361  stoweidlem62  31733  cvlcvr1  34804  llnmlplnN  35003  cdlemb  35258  paddasslem10  35293  trlcnv  35630  trlator0  35636  trlid0  35641  trlnidatb  35642  cdlemd4  35666  cdlemg5  36071  trlco  36193  cdlemj3  36289  tendo0mul  36292  tendo0mulr  36293  tendoconid  36295  erngdv  36459  erngdv-rN  36467  dihmeetlem1N  36757  dihatlat  36801  hgmaprnlem5N  37370  imo72b2lem1  37657
  Copyright terms: Public domain W3C validator