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

Theorem rexlimddv 3288
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 3282 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2105  wrex 3136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-ral 3140  df-rex 3141
This theorem is referenced by:  oaabs2  8261  oemapvali  9135  cantnflem4  9143  r1pwss  9201  djuun  9343  infxpenc2lem1  9433  pwfseqlem3  10070  prlem934  10443  ltexprlem7  10452  reclem3pr  10459  00id  10803  mul02lem1  10804  addid2  10811  addcan  10812  addcan2  10813  negeu  10864  mulcand  11261  suprzcl  12050  uzwo3  12331  expmulnbnd  13584  limsupgre  14826  rlimclim1  14890  fsumcvg3  15074  oexpneg  15682  bitsfi  15774  vdwlem10  16314  mreexexlem4d  16906  mreexdomd  16908  isacs3lem  17764  grprinvlem  17871  grpridd  17873  grprcan  18075  sylow1  18657  pgpfi  18659  slwhash  18678  pj1id  18754  efgsfo  18794  efgredlemc  18800  dmdprdsplitlem  19088  dpjidcl  19109  pgpfac1lem4  19129  pgpfaclem2  19133  pgpfaclem3  19134  ablsimpgcygd  19157  ablsimpgfindlem1  19158  ablsimpgfind  19161  fincygsubgodexd  19164  ablsimpgprmd  19166  gsummgp0  19287  lspsolv  19844  restbas  21694  restcls  21717  restntr  21718  cnpnei  21800  cnpco  21803  pnrmopn  21879  1stcfb  21981  1stcrest  21989  2ndcctbss  21991  2ndcomap  21994  dis2ndc  21996  llyidm  22024  nllyidm  22025  hausllycmp  22030  lly1stc  22032  llycmpkgen2  22086  1stckgenlem  22089  basqtop  22247  regr1lem  22275  kqreglem1  22277  kqreglem2  22278  kqnrmlem1  22279  kqnrmlem2  22280  reghmph  22329  nrmhmph  22330  qtophmeo  22353  trfbas2  22379  fbasfip  22404  fbasrn  22420  trfg  22427  ssufl  22454  fmufil  22495  ufldom  22498  uffclsflim  22567  cnpfcfi  22576  alexsublem  22580  alexsubALTlem4  22586  ptcmplem3  22590  ptcmplem4  22591  tsmsxp  22690  met1stc  23058  met2ndci  23059  prdsxmslem2  23066  metcnpi3  23083  icccmplem1  23357  xrge0tsms  23369  metdseq0  23389  cnllycmp  23487  bndth  23489  lebnumlem1  23492  lebnum  23495  cfilfcls  23804  lmle  23831  relcmpcmet  23848  pjthlem2  23968  ovolscalem2  24042  ovolicc2lem4  24048  ovolicc2lem5  24049  ioombl1  24090  uniioombllem6  24116  uniioombl  24117  opnmbllem  24129  volivth  24135  mbfinf  24193  mbfi1fseqlem6  24248  itg2cnlem1  24289  itg2cn  24291  lhop2  24539  dvcnvre  24543  aareccl  24842  aaliou3lem8  24861  aaliou3lem9  24866  ulmdvlem3  24917  mtestbdd  24920  iblulm  24922  radcnvlem1  24928  abelthlem5  24950  abelthlem8  24954  chordthm  25342  dcubic  25351  lgambdd  25541  lgamucov  25542  lgamcvglem  25544  lgamcvg2  25559  fta  25584  dchrptlem2  25768  sumdchr2  25773  2sqlem11  25932  dchrisum  25995  dchrisum0flb  26013  pntibndlem3  26095  pntlemi  26107  pjspansn  29281  chscllem3  29343  xmulcand  30524  xrge0tsmsd  30619  esumpcvgval  31236  cnpconn  32374  pconnconn  32375  connpconn  32379  pconnpi1  32381  cnllysconn  32389  cvmcov2  32419  cvmliftpht  32462  mthmpps  32726  sinccvg  32813  btwnconn1lem13  33457  neibastop2lem  33605  tailfb  33622  unblimceq0lem  33742  knoppndvlem9  33756  knoppndvlem21  33768  knoppndvlem22  33769  matunitlindflem2  34770  poimirlem29  34802  opnmbllem0  34809  mblfinlem2  34811  mblfinlem4  34813  prdsbnd2  34954  cntotbnd  34955  heiborlem8  34977  heiborlem9  34978  cvlcvr1  36355  llnmlplnN  36555  cdlemb  36810  paddasslem10  36845  trlcnv  37181  trlator0  37187  trlid0  37192  trlnidatb  37193  cdlemd4  37217  cdlemg5  37621  trlco  37743  cdlemj3  37839  tendo0mul  37842  tendo0mulr  37843  tendoconid  37845  erngdv  38009  erngdv-rN  38017  dihmeetlem1N  38306  dihatlat  38350  hgmaprnlem5N  38916  remulcan2d  39034  renegeulemv  39076  remul02  39113  remul01  39115  remulinvcom  39126  remulid2  39127  remulcand  39128  prjspertr  39133  0prjspnrel  39147  acongrep  39455  jm2.27b  39481  lmhmfgsplit  39564  hbt  39608  imo72b2lem1  40399  mnuss2d  40477  mnuprdlem4  40488  mnuunid  40490  mnurndlem2  40495  cncmpmax  41166  rexlimddv2  41980  stoweidlem62  42224  oexpnegALTV  43719  oexpnegnz  43720  aacllem  44830
  Copyright terms: Public domain W3C validator