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

Theorem rexlimddv 2836
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 2833 . 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 360    e. wcel 1726   E.wrex 2708
This theorem is referenced by:  grprinvlem  6288  grpridd  6290  oaabs2  6891  oemapvali  7643  cantnflem4  7651  r1pwss  7713  infxpenc2lem1  7905  pwfseqlem3  8540  prlem934  8915  ltexprlem7  8924  reclem3pr  8931  00id  9246  mul02lem1  9247  addid2  9254  addcan  9255  addcan2  9256  negeu  9301  mulcand  9660  suprzcl  10354  uzwo3  10574  expmulnbnd  11516  limsupgre  12280  rlimclim1  12344  fsumcvg3  12528  oexpneg  12916  bitsfi  12954  vdwlem10  13363  mreexexlem4d  13877  mreexdomd  13879  isacs3lem  14597  grprcan  14843  sylow1  15242  pgpfi  15244  slwhash  15263  pj1id  15336  efgsfo  15376  efgredlemc  15382  dmdprdsplitlem  15600  dpjidcl  15621  pgpfac1lem4  15641  pgpfaclem2  15645  pgpfaclem3  15646  lspsolv  16220  restbas  17227  restcls  17250  restntr  17251  cnpnei  17333  cnpco  17336  pnrmopn  17412  1stcfb  17513  1stcrest  17521  2ndcctbss  17523  2ndcomap  17526  dis2ndc  17528  llyidm  17556  nllyidm  17557  hausllycmp  17562  lly1stc  17564  llycmpkgen2  17587  1stckgenlem  17590  basqtop  17748  regr1lem  17776  kqreglem1  17778  kqreglem2  17779  kqnrmlem1  17780  kqnrmlem2  17781  reghmph  17830  nrmhmph  17831  qtophmeo  17854  trfbas2  17880  fbasfip  17905  fbasrn  17921  trfg  17928  ssufl  17955  fmufil  17996  ufldom  17999  uffclsflim  18068  cnpfcfi  18077  alexsublem  18080  alexsubALTlem4  18086  ptcmplem3  18090  ptcmplem4  18091  tsmsxp  18189  met1stc  18556  met2ndci  18557  prdsxmslem2  18564  metcnpi3  18581  icccmplem1  18858  xrge0tsms  18870  metdseq0  18889  cnllycmp  18986  bndth  18988  lebnumlem1  18991  lebnum  18994  cfilfcls  19232  lmle  19259  relcmpcmet  19274  pjthlem2  19344  ovolscalem2  19415  ovolicc2lem4  19421  ovolicc2lem5  19422  ioombl1  19461  uniioombllem6  19485  uniioombl  19486  opnmbllem  19498  volivth  19504  mbfinf  19560  mbfi1fseqlem6  19615  itg2cnlem1  19656  itg2cn  19658  lhop2  19904  dvcnvre  19908  aareccl  20248  aaliou3lem8  20267  aaliou3lem9  20272  ulmdvlem3  20323  mtestbdd  20326  iblulm  20328  radcnvlem1  20334  abelthlem5  20356  abelthlem8  20360  chordthm  20683  dcubic  20691  fta  20867  dchrptlem2  21054  sumdchr2  21059  2sqlem11  21164  dchrisum  21191  dchrisum0flb  21209  pntibndlem3  21291  pntlemi  21303  pjspansn  23084  chscllem3  23146  xmulcand  24172  xrge0tsmsd  24228  esumpcvgval  24473  lgambdd  24826  lgamucov  24827  lgamcvglem  24829  lgamcvg2  24844  cnpcon  24922  pconcon  24923  conpcon  24927  pconpi1  24929  cnllyscon  24937  cvmcov2  24967  cvmliftpht  25010  sinccvg  25115  btwnconn1lem13  26038  opnmbllem0  26254  mblfinlem2  26256  mblfinlem4  26258  neibastop2lem  26403  tailfb  26420  prdsbnd2  26518  cntotbnd  26519  heiborlem8  26541  heiborlem9  26542  acongrep  27059  jm2.27b  27091  lmhmfgsplit  27175  hbt  27325  cncmpmax  27693  stoweidlem62  27801  cvlcvr1  30211  llnmlplnN  30410  cdlemb  30665  paddasslem10  30700  trlcnv  31036  trlator0  31042  trlid0  31047  trlnidatb  31048  cdlemd4  31072  cdlemg5  31476  trlco  31598  cdlemj3  31694  tendo0mul  31697  tendo0mulr  31698  tendoconid  31700  erngdv  31864  erngdv-rN  31872  dihmeetlem1N  32162  dihatlat  32206  hgmaprnlem5N  32775
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-11 1762
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-nf 1555  df-ral 2712  df-rex 2713
  Copyright terms: Public domain W3C validator