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

Theorem rexlimddv 3173
Description: Restricted existential elimination rule of natural deduction. (Contributed by Mario Carneiro, 15-Jun-2016.)
Hypotheses
Ref Expression
rexlimddv.1 (𝜑 → ∃𝑥𝐴 𝜓)
rexlimddv.2 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
Assertion
Ref Expression
rexlimddv (𝜑𝜒)
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimddv
StepHypRef Expression
1 rexlimddv.1 . 2 (𝜑 → ∃𝑥𝐴 𝜓)
2 rexlimddv.2 . . 3 ((𝜑 ∧ (𝑥𝐴𝜓)) → 𝜒)
32rexlimdvaa 3170 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2139  wrex 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-ral 3055  df-rex 3056
This theorem is referenced by:  grprinvlem  7038  grpridd  7040  oaabs2  7896  oemapvali  8756  cantnflem4  8764  r1pwss  8822  djuun  8962  infxpenc2lem1  9052  pwfseqlem3  9694  prlem934  10067  ltexprlem7  10076  reclem3pr  10083  00id  10423  mul02lem1  10424  addid2  10431  addcan  10432  addcan2  10433  negeu  10483  mulcand  10872  suprzcl  11669  uzwo3  11996  expmulnbnd  13210  limsupgre  14431  rlimclim1  14495  fsumcvg3  14679  oexpneg  15291  bitsfi  15381  vdwlem10  15916  mreexexlem4d  16529  mreexdomd  16531  isacs3lem  17387  grprcan  17676  sylow1  18238  pgpfi  18240  slwhash  18259  pj1id  18332  efgsfo  18372  efgredlemc  18378  dmdprdsplitlem  18656  dpjidcl  18677  pgpfac1lem4  18697  pgpfaclem2  18701  pgpfaclem3  18702  gsummgp0  18828  lspsolv  19365  restbas  21184  restcls  21207  restntr  21208  cnpnei  21290  cnpco  21293  pnrmopn  21369  1stcfb  21470  1stcrest  21478  2ndcctbss  21480  2ndcomap  21483  dis2ndc  21485  llyidm  21513  nllyidm  21514  hausllycmp  21519  lly1stc  21521  llycmpkgen2  21575  1stckgenlem  21578  basqtop  21736  regr1lem  21764  kqreglem1  21766  kqreglem2  21767  kqnrmlem1  21768  kqnrmlem2  21769  reghmph  21818  nrmhmph  21819  qtophmeo  21842  trfbas2  21868  fbasfip  21893  fbasrn  21909  trfg  21916  ssufl  21943  fmufil  21984  ufldom  21987  uffclsflim  22056  cnpfcfi  22065  alexsublem  22069  alexsubALTlem4  22075  ptcmplem3  22079  ptcmplem4  22080  tsmsxp  22179  met1stc  22547  met2ndci  22548  prdsxmslem2  22555  metcnpi3  22572  icccmplem1  22846  xrge0tsms  22858  metdseq0  22878  cnllycmp  22976  bndth  22978  lebnumlem1  22981  lebnum  22984  cfilfcls  23292  lmle  23319  relcmpcmet  23335  pjthlem2  23429  ovolscalem2  23502  ovolicc2lem4  23508  ovolicc2lem5  23509  ioombl1  23550  uniioombllem6  23576  uniioombl  23577  opnmbllem  23589  volivth  23595  mbfinf  23651  mbfi1fseqlem6  23706  itg2cnlem1  23747  itg2cn  23749  lhop2  23997  dvcnvre  24001  aareccl  24300  aaliou3lem8  24319  aaliou3lem9  24324  ulmdvlem3  24375  mtestbdd  24378  iblulm  24380  radcnvlem1  24386  abelthlem5  24408  abelthlem8  24412  chordthm  24784  dcubic  24793  lgambdd  24983  lgamucov  24984  lgamcvglem  24986  lgamcvg2  25001  fta  25026  dchrptlem2  25210  sumdchr2  25215  2sqlem11  25374  dchrisum  25401  dchrisum0flb  25419  pntibndlem3  25501  pntlemi  25513  pjspansn  28766  chscllem3  28828  xmulcand  29959  xrge0tsmsd  30115  esumpcvgval  30470  cnpconn  31540  pconnconn  31541  connpconn  31545  pconnpi1  31547  cnllysconn  31555  cvmcov2  31585  cvmliftpht  31628  mthmpps  31807  sinccvg  31895  btwnconn1lem13  32533  neibastop2lem  32682  tailfb  32699  unblimceq0lem  32824  knoppndvlem9  32838  knoppndvlem21  32850  knoppndvlem22  32851  matunitlindflem2  33737  poimirlem29  33769  opnmbllem0  33776  mblfinlem2  33778  mblfinlem4  33780  prdsbnd2  33925  cntotbnd  33926  heiborlem8  33948  heiborlem9  33949  cvlcvr1  35147  llnmlplnN  35346  cdlemb  35601  paddasslem10  35636  trlcnv  35973  trlator0  35979  trlid0  35984  trlnidatb  35985  cdlemd4  36009  cdlemg5  36413  trlco  36535  cdlemj3  36631  tendo0mul  36634  tendo0mulr  36635  tendoconid  36637  erngdv  36801  erngdv-rN  36809  dihmeetlem1N  37099  dihatlat  37143  hgmaprnlem5N  37712  acongrep  38067  jm2.27b  38093  lmhmfgsplit  38176  hbt  38220  imo72b2lem1  38991  cncmpmax  39708  rexlimddv2  40570  stoweidlem62  40800  oexpnegALTV  42116  oexpnegnz  42117  aacllem  43078
  Copyright terms: Public domain W3C validator