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

Theorem rexlimddv 3156
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 3151 . 2 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
41, 3mpd 15 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wcel 2106  wrex 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913
This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-rex 3072
This theorem is referenced by:  frxp2  8072  frxp3  8079  oaabs2  8591  oemapvali  9616  cantnflem4  9624  r1pwss  9716  djuun  9858  infxpenc2lem1  9951  pwfseqlem3  10592  prlem934  10965  ltexprlem7  10974  reclem3pr  10981  00id  11326  mul02lem1  11327  addid2  11334  addcan  11335  addcan2  11336  negeu  11387  mulcand  11784  suprzcl  12579  uzwo3  12860  expmulnbnd  14130  limsupgre  15355  rlimclim1  15419  fsumcvg3  15606  oexpneg  16219  bitsfi  16309  vdwlem10  16854  mreexexlem4d  17519  mreexdomd  17521  isacs3lem  18423  grprinvlem  18520  grpridd  18522  grprcan  18776  sylow1  19376  pgpfi  19378  slwhash  19397  pj1id  19472  efgsfo  19512  efgredlemc  19518  dmdprdsplitlem  19807  dpjidcl  19828  pgpfac1lem4  19848  pgpfaclem2  19852  pgpfaclem3  19853  ablsimpgcygd  19876  ablsimpgfindlem1  19877  ablsimpgfind  19880  fincygsubgodexd  19883  ablsimpgprmd  19885  gsummgp0  20017  lspsolv  20589  restbas  22493  restcls  22516  restntr  22517  cnpnei  22599  cnpco  22602  pnrmopn  22678  1stcfb  22780  1stcrest  22788  2ndcctbss  22790  2ndcomap  22793  dis2ndc  22795  llyidm  22823  nllyidm  22824  hausllycmp  22829  lly1stc  22831  llycmpkgen2  22885  1stckgenlem  22888  basqtop  23046  regr1lem  23074  kqreglem1  23076  kqreglem2  23077  kqnrmlem1  23078  kqnrmlem2  23079  reghmph  23128  nrmhmph  23129  qtophmeo  23152  trfbas2  23178  fbasfip  23203  fbasrn  23219  trfg  23226  ssufl  23253  fmufil  23294  ufldom  23297  uffclsflim  23366  cnpfcfi  23375  alexsublem  23379  alexsubALTlem4  23385  ptcmplem3  23389  ptcmplem4  23390  tsmsxp  23490  met1stc  23861  met2ndci  23862  prdsxmslem2  23869  metcnpi3  23886  icccmplem1  24169  xrge0tsms  24181  metdseq0  24201  cnllycmp  24303  bndth  24305  lebnumlem1  24308  lebnum  24311  cfilfcls  24622  lmle  24649  relcmpcmet  24666  pjthlem2  24786  ovolscalem2  24862  ovolicc2lem4  24868  ovolicc2lem5  24869  ioombl1  24910  uniioombllem6  24936  uniioombl  24937  opnmbllem  24949  volivth  24955  mbfinf  25013  mbfi1fseqlem6  25069  itg2cnlem1  25110  itg2cn  25112  lhop2  25363  dvcnvre  25367  aareccl  25670  aaliou3lem8  25689  aaliou3lem9  25694  ulmdvlem3  25745  mtestbdd  25748  iblulm  25750  radcnvlem1  25756  abelthlem5  25778  abelthlem8  25782  chordthm  26171  dcubic  26180  lgambdd  26370  lgamucov  26371  lgamcvglem  26373  lgamcvg2  26388  fta  26413  dchrptlem2  26597  sumdchr2  26602  2sqlem11  26761  dchrisum  26824  dchrisum0flb  26842  pntibndlem3  26924  pntlemi  26936  scutbdaybnd  27138  cofsslt  27221  coinitsslt  27222  pjspansn  30405  chscllem3  30467  xmulcand  31660  xrge0tsmsd  31782  esumpcvgval  32546  cnpconn  33693  pconnconn  33694  connpconn  33698  pconnpi1  33700  cnllysconn  33708  cvmcov2  33738  cvmliftpht  33781  mthmpps  34045  sinccvg  34130  addsproplem6  34290  negsproplem6  34335  btwnconn1lem13  34651  neibastop2lem  34799  tailfb  34816  unblimceq0lem  34936  knoppndvlem9  34950  knoppndvlem21  34962  knoppndvlem22  34963  matunitlindflem2  36042  poimirlem29  36074  opnmbllem0  36081  mblfinlem2  36083  mblfinlem4  36085  prdsbnd2  36221  cntotbnd  36222  heiborlem8  36244  heiborlem9  36245  cvlcvr1  37768  llnmlplnN  37969  cdlemb  38224  paddasslem10  38259  trlcnv  38595  trlator0  38601  trlid0  38606  trlnidatb  38607  cdlemd4  38631  cdlemg5  39035  trlco  39157  cdlemj3  39253  tendo0mul  39256  tendo0mulr  39257  tendoconid  39259  erngdv  39423  erngdv-rN  39431  dihmeetlem1N  39720  dihatlat  39764  hgmaprnlem5N  40330  rncrhmcl  40667  remulcan2d  40717  renegeulemv  40775  remul02  40812  remul01  40814  sn-addcand  40826  sn-addid1  40827  sn-addcan2d  40828  sn-subeu  40833  remulinvcom  40839  remulid2  40840  remulcand  40845  sn-0tie0  40846  itrere  40873  retire  40874  prjspertr  40881  0prjspnrel  40903  acongrep  41242  jm2.27b  41268  lmhmfgsplit  41351  hbt  41395  imo72b2lem1  42384  mnuss2d  42486  mnuprdlem4  42497  mnuunid  42499  mnurndlem2  42504  cncmpmax  43179  rexlimddv2  43996  stoweidlem62  44235  salrestss  44534  oexpnegALTV  45801  oexpnegnz  45802  aacllem  47180
  Copyright terms: Public domain W3C validator