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

Theorem rexlimddv 2918
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 2915 . 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 370    e. wcel 1872   E.wrex 2772
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1658  df-ral 2776  df-rex 2777
This theorem is referenced by:  grprinvlem  6521  grpridd  6523  oaabs2  7357  oemapvali  8197  cantnflem4  8205  r1pwss  8263  infxpenc2lem1  8457  pwfseqlem3  9092  prlem934  9465  ltexprlem7  9474  reclem3pr  9481  00id  9815  mul02lem1  9816  addid2  9823  addcan  9824  addcan2  9825  negeu  9872  mulcand  10252  suprzcl  11022  uzwo3  11266  expmulnbnd  12410  limsupgre  13541  limsupgreOLD  13542  rlimclim1  13608  fsumcvg3  13794  oexpneg  14367  bitsfi  14410  vdwlem10  14939  mreexexlem4d  15552  mreexdomd  15554  isacs3lem  16411  grprcan  16698  sylow1  17254  pgpfi  17256  slwhash  17275  pj1id  17348  efgsfo  17388  efgredlemc  17394  dmdprdsplitlem  17669  dpjidcl  17690  pgpfac1lem4  17710  pgpfaclem2  17714  pgpfaclem3  17715  gsummgp0  17835  lspsolv  18365  restbas  20172  restcls  20195  restntr  20196  cnpnei  20278  cnpco  20281  pnrmopn  20357  1stcfb  20458  1stcrest  20466  2ndcctbss  20468  2ndcomap  20471  dis2ndc  20473  llyidm  20501  nllyidm  20502  hausllycmp  20507  lly1stc  20509  llycmpkgen2  20563  1stckgenlem  20566  basqtop  20724  regr1lem  20752  kqreglem1  20754  kqreglem2  20755  kqnrmlem1  20756  kqnrmlem2  20757  reghmph  20806  nrmhmph  20807  qtophmeo  20830  trfbas2  20856  fbasfip  20881  fbasrn  20897  trfg  20904  ssufl  20931  fmufil  20972  ufldom  20975  uffclsflim  21044  cnpfcfi  21053  alexsublem  21057  alexsubALTlem4  21063  ptcmplem3  21067  ptcmplem4  21068  tsmsxp  21167  met1stc  21534  met2ndci  21535  prdsxmslem2  21542  metcnpi3  21559  icccmplem1  21838  xrge0tsms  21850  metdseq0  21869  metdseq0OLD  21884  cnllycmp  21982  bndth  21984  lebnumlem1  21987  lebnumlem1OLD  21990  lebnum  21993  cfilfcls  22242  lmle  22269  relcmpcmet  22284  pjthlem2  22390  ovolscalem2  22465  ovolicc2lem4OLD  22471  ovolicc2lem4  22472  ovolicc2lem5  22473  ioombl1  22513  uniioombllem6  22544  uniioombl  22545  opnmbllem  22557  volivth  22563  mbfinf  22619  mbfinfOLD  22620  mbfi1fseqlem6  22676  itg2cnlem1  22717  itg2cn  22719  lhop2  22965  dvcnvre  22969  aareccl  23280  aaliou3lem8  23299  aaliou3lem9  23304  ulmdvlem3  23355  mtestbdd  23358  iblulm  23360  radcnvlem1  23366  abelthlem5  23388  abelthlem8  23392  chordthm  23761  dcubic  23770  lgambdd  23960  lgamucov  23961  lgamcvglem  23963  lgamcvg2  23978  fta  24004  dchrptlem2  24191  sumdchr2  24196  2sqlem11  24301  dchrisum  24328  dchrisum0flb  24346  pntibndlem3  24428  pntlemi  24440  pjspansn  27228  chscllem3  27290  xmulcand  28397  xrge0tsmsd  28556  esumpcvgval  28907  cnpcon  29961  pconcon  29962  conpcon  29966  pconpi1  29968  cnllyscon  29976  cvmcov2  30006  cvmliftpht  30049  mthmpps  30228  sinccvg  30325  btwnconn1lem13  30871  neibastop2lem  31021  tailfb  31038  poimirlem29  31933  opnmbllem0  31940  mblfinlem2  31942  mblfinlem4  31944  prdsbnd2  32091  cntotbnd  32092  heiborlem8  32114  heiborlem9  32115  cvlcvr1  32874  llnmlplnN  33073  cdlemb  33328  paddasslem10  33363  trlcnv  33700  trlator0  33706  trlid0  33711  trlnidatb  33712  cdlemd4  33736  cdlemg5  34141  trlco  34263  cdlemj3  34359  tendo0mul  34362  tendo0mulr  34363  tendoconid  34365  erngdv  34529  erngdv-rN  34537  dihmeetlem1N  34827  dihatlat  34871  hgmaprnlem5N  35440  acongrep  35800  jm2.27b  35831  lmhmfgsplit  35914  hbt  35959  imo72b2lem1  36584  cncmpmax  37326  stoweidlem62  37863  stoweidlem62OLD  37864  oexpnegALTV  38676  oexpnegnz  38677  aacllem  40161
  Copyright terms: Public domain W3C validator