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

Theorem rexlimddv 3064
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 3061 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  wcel 2030  wrex 2942
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-ral 2946  df-rex 2947
This theorem is referenced by:  grprinvlem  6914  grpridd  6916  oaabs2  7770  oemapvali  8619  cantnflem4  8627  r1pwss  8685  infxpenc2lem1  8880  pwfseqlem3  9520  prlem934  9893  ltexprlem7  9902  reclem3pr  9909  00id  10249  mul02lem1  10250  addid2  10257  addcan  10258  addcan2  10259  negeu  10309  mulcand  10698  suprzcl  11495  uzwo3  11821  expmulnbnd  13036  limsupgre  14256  rlimclim1  14320  fsumcvg3  14504  oexpneg  15116  bitsfi  15206  vdwlem10  15741  mreexexlem4d  16354  mreexdomd  16357  isacs3lem  17213  grprcan  17502  sylow1  18064  pgpfi  18066  slwhash  18085  pj1id  18158  efgsfo  18198  efgredlemc  18204  dmdprdsplitlem  18482  dpjidcl  18503  pgpfac1lem4  18523  pgpfaclem2  18527  pgpfaclem3  18528  gsummgp0  18654  lspsolv  19191  restbas  21010  restcls  21033  restntr  21034  cnpnei  21116  cnpco  21119  pnrmopn  21195  1stcfb  21296  1stcrest  21304  2ndcctbss  21306  2ndcomap  21309  dis2ndc  21311  llyidm  21339  nllyidm  21340  hausllycmp  21345  lly1stc  21347  llycmpkgen2  21401  1stckgenlem  21404  basqtop  21562  regr1lem  21590  kqreglem1  21592  kqreglem2  21593  kqnrmlem1  21594  kqnrmlem2  21595  reghmph  21644  nrmhmph  21645  qtophmeo  21668  trfbas2  21694  fbasfip  21719  fbasrn  21735  trfg  21742  ssufl  21769  fmufil  21810  ufldom  21813  uffclsflim  21882  cnpfcfi  21891  alexsublem  21895  alexsubALTlem4  21901  ptcmplem3  21905  ptcmplem4  21906  tsmsxp  22005  met1stc  22373  met2ndci  22374  prdsxmslem2  22381  metcnpi3  22398  icccmplem1  22672  xrge0tsms  22684  metdseq0  22704  cnllycmp  22802  bndth  22804  lebnumlem1  22807  lebnum  22810  cfilfcls  23118  lmle  23145  relcmpcmet  23161  pjthlem2  23255  ovolscalem2  23328  ovolicc2lem4  23334  ovolicc2lem5  23335  ioombl1  23376  uniioombllem6  23402  uniioombl  23403  opnmbllem  23415  volivth  23421  mbfinf  23477  mbfi1fseqlem6  23532  itg2cnlem1  23573  itg2cn  23575  lhop2  23823  dvcnvre  23827  aareccl  24126  aaliou3lem8  24145  aaliou3lem9  24150  ulmdvlem3  24201  mtestbdd  24204  iblulm  24206  radcnvlem1  24212  abelthlem5  24234  abelthlem8  24238  chordthm  24609  dcubic  24618  lgambdd  24808  lgamucov  24809  lgamcvglem  24811  lgamcvg2  24826  fta  24851  dchrptlem2  25035  sumdchr2  25040  2sqlem11  25199  dchrisum  25226  dchrisum0flb  25244  pntibndlem3  25326  pntlemi  25338  pjspansn  28564  chscllem3  28626  xmulcand  29757  xrge0tsmsd  29913  esumpcvgval  30268  cnpconn  31338  pconnconn  31339  connpconn  31343  pconnpi1  31345  cnllysconn  31353  cvmcov2  31383  cvmliftpht  31426  mthmpps  31605  sinccvg  31693  btwnconn1lem13  32331  neibastop2lem  32480  tailfb  32497  unblimceq0lem  32622  knoppndvlem9  32636  knoppndvlem21  32648  knoppndvlem22  32649  matunitlindflem2  33536  poimirlem29  33568  opnmbllem0  33575  mblfinlem2  33577  mblfinlem4  33579  prdsbnd2  33724  cntotbnd  33725  heiborlem8  33747  heiborlem9  33748  cvlcvr1  34944  llnmlplnN  35143  cdlemb  35398  paddasslem10  35433  trlcnv  35770  trlator0  35776  trlid0  35781  trlnidatb  35782  cdlemd4  35806  cdlemg5  36210  trlco  36332  cdlemj3  36428  tendo0mul  36431  tendo0mulr  36432  tendoconid  36434  erngdv  36598  erngdv-rN  36606  dihmeetlem1N  36896  dihatlat  36940  hgmaprnlem5N  37509  acongrep  37864  jm2.27b  37890  lmhmfgsplit  37973  hbt  38017  imo72b2lem1  38788  cncmpmax  39505  rexlimddv2  40367  stoweidlem62  40597  oexpnegALTV  41913  oexpnegnz  41914  aacllem  42875
  Copyright terms: Public domain W3C validator