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

Theorem rexlimddv 2928
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 2925 . 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 1870   E.wrex 2783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751
This theorem depends on definitions:  df-bi 188  df-an 372  df-ex 1660  df-ral 2787  df-rex 2788
This theorem is referenced by:  grprinvlem  6521  grpridd  6523  oaabs2  7354  oemapvali  8188  cantnflem4  8196  r1pwss  8254  infxpenc2lem1  8448  pwfseqlem3  9084  prlem934  9457  ltexprlem7  9466  reclem3pr  9473  00id  9807  mul02lem1  9808  addid2  9815  addcan  9816  addcan2  9817  negeu  9864  mulcand  10244  suprzcl  11015  uzwo3  11259  expmulnbnd  12401  limsupgre  13520  limsupgreOLD  13521  rlimclim1  13587  fsumcvg3  13773  oexpneg  14346  bitsfi  14385  vdwlem10  14903  mreexexlem4d  15504  mreexdomd  15506  isacs3lem  16363  grprcan  16650  sylow1  17190  pgpfi  17192  slwhash  17211  pj1id  17284  efgsfo  17324  efgredlemc  17330  dmdprdsplitlem  17605  dpjidcl  17626  pgpfac1lem4  17646  pgpfaclem2  17650  pgpfaclem3  17651  gsummgp0  17771  lspsolv  18301  restbas  20105  restcls  20128  restntr  20129  cnpnei  20211  cnpco  20214  pnrmopn  20290  1stcfb  20391  1stcrest  20399  2ndcctbss  20401  2ndcomap  20404  dis2ndc  20406  llyidm  20434  nllyidm  20435  hausllycmp  20440  lly1stc  20442  llycmpkgen2  20496  1stckgenlem  20499  basqtop  20657  regr1lem  20685  kqreglem1  20687  kqreglem2  20688  kqnrmlem1  20689  kqnrmlem2  20690  reghmph  20739  nrmhmph  20740  qtophmeo  20763  trfbas2  20789  fbasfip  20814  fbasrn  20830  trfg  20837  ssufl  20864  fmufil  20905  ufldom  20908  uffclsflim  20977  cnpfcfi  20986  alexsublem  20990  alexsubALTlem4  20996  ptcmplem3  21000  ptcmplem4  21001  tsmsxp  21100  met1stc  21467  met2ndci  21468  prdsxmslem2  21475  metcnpi3  21492  icccmplem1  21751  xrge0tsms  21763  metdseq0  21782  cnllycmp  21880  bndth  21882  lebnumlem1  21885  lebnum  21888  cfilfcls  22137  lmle  22164  relcmpcmet  22179  pjthlem2  22273  ovolscalem2  22345  ovolicc2lem4  22351  ovolicc2lem5  22352  ioombl1  22392  uniioombllem6  22423  uniioombl  22424  opnmbllem  22436  volivth  22442  mbfinf  22498  mbfinfOLD  22499  mbfi1fseqlem6  22555  itg2cnlem1  22596  itg2cn  22598  lhop2  22844  dvcnvre  22848  aareccl  23147  aaliou3lem8  23166  aaliou3lem9  23171  ulmdvlem3  23222  mtestbdd  23225  iblulm  23227  radcnvlem1  23233  abelthlem5  23255  abelthlem8  23259  chordthm  23628  dcubic  23637  lgambdd  23827  lgamucov  23828  lgamcvglem  23830  lgamcvg2  23845  fta  23869  dchrptlem2  24056  sumdchr2  24061  2sqlem11  24166  dchrisum  24193  dchrisum0flb  24211  pntibndlem3  24293  pntlemi  24305  pjspansn  27065  chscllem3  27127  xmulcand  28228  xrge0tsmsd  28387  esumpcvgval  28738  cnpcon  29741  pconcon  29742  conpcon  29746  pconpi1  29748  cnllyscon  29756  cvmcov2  29786  cvmliftpht  29829  mthmpps  30008  sinccvg  30105  btwnconn1lem13  30651  neibastop2lem  30801  tailfb  30818  poimirlem29  31673  opnmbllem0  31680  mblfinlem2  31682  mblfinlem4  31684  prdsbnd2  31831  cntotbnd  31832  heiborlem8  31854  heiborlem9  31855  cvlcvr1  32614  llnmlplnN  32813  cdlemb  33068  paddasslem10  33103  trlcnv  33440  trlator0  33446  trlid0  33451  trlnidatb  33452  cdlemd4  33476  cdlemg5  33881  trlco  34003  cdlemj3  34099  tendo0mul  34102  tendo0mulr  34103  tendoconid  34105  erngdv  34269  erngdv-rN  34277  dihmeetlem1N  34567  dihatlat  34611  hgmaprnlem5N  35180  acongrep  35536  jm2.27b  35567  lmhmfgsplit  35650  hbt  35695  imo72b2lem1  36251  cncmpmax  36993  stoweidlem62  37492  stoweidlem62OLD  37493  oexpnegALTV  38196  oexpnegnz  38197  aacllem  39301
  Copyright terms: Public domain W3C validator