ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  rexlimdva GIF version

Theorem rexlimdva 2547
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
rexlimdva (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Distinct variable groups:   𝜑,𝑥   𝜒,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝐴(𝑥)

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3 ((𝜑𝑥𝐴) → (𝜓𝜒))
21ex 114 . 2 (𝜑 → (𝑥𝐴 → (𝜓𝜒)))
32rexlimdv 2546 1 (𝜑 → (∃𝑥𝐴 𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wcel 1480  wrex 2415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2419  df-rex 2420
This theorem is referenced by:  rexlimdvaa  2548  rexlimivv  2553  rexlimdvv  2554  ralxfrd  4378  rexxfrd  4379  fvelimab  5470  foco2  5648  elunirn  5660  f1elima  5667  tfrlem5  6204  tfrlemibacc  6216  tfrlemibfn  6218  tfr1onlembacc  6232  tfr1onlembfn  6234  tfrcllembacc  6245  tfrcllembfn  6247  frecabcl  6289  nnaordex  6416  nnawordex  6417  ectocld  6488  phpm  6752  dif1enen  6767  fin0  6772  fin0or  6773  fimax2gtri  6788  fidcenum  6837  suplub2ti  6881  supisoex  6889  enomnilem  7003  finomni  7005  exmidfodomrlemeldju  7048  exmidfodomrlemreseldju  7049  ltexnqq  7209  ltbtwnnqq  7216  prarloclem4  7299  prarloc2  7305  genprndl  7322  genprndu  7323  prmuloc2  7368  1idprl  7391  1idpru  7392  cauappcvgprlemdisj  7452  cauappcvgprlemladdru  7457  cauappcvgprlemladdrl  7458  caucvgprlemladdrl  7479  recexgt0sr  7574  map2psrprg  7606  suplocsrlem  7609  nntopi  7695  cnegexlem1  7930  cnegexlem2  7931  renegcl  8016  supinfneg  9383  infsupneg  9384  qmulz  9408  icc0r  9702  exbtwnzlemstep  10018  rebtwn2zlemstep  10023  ioo0  10030  ico0  10032  ioc0  10033  modqmuladd  10132  addmodlteq  10164  frec2uzrand  10171  frecuzrdgtcl  10178  frecuzrdgfunlem  10185  hashunlem  10543  shftlem  10581  caucvgre  10746  resqrexlemgt0  10785  rexico  10986  negfi  10992  climuni  11055  climshftlemg  11064  climcn1  11070  serf0  11114  summodclem2  11144  zsumdc  11146  fsum2dlemstep  11196  mertenslem2  11298  ntrivcvgap  11310  dvds1lem  11493  odd2np1lem  11558  odd2np1  11559  sqoddm1div8z  11572  ltoddhalfle  11579  halfleoddlt  11580  m1expo  11586  divalglemeunn  11607  divalglemex  11608  divalglemeuneg  11609  flodddiv4  11620  bezoutlemaz  11680  bezoutlembz  11681  dvdssqim  11701  ncoprmgcdne1b  11759  coprmdvds2  11763  divgcdcoprm0  11771  cncongr1  11773  cncongr2  11774  dvdsnprmd  11795  rpexp  11820  tgcl  12222  innei  12321  cnptoprest  12397  lmss  12404  lmtopcnp  12408  txlm  12437  blssps  12585  blss  12586  blssexps  12587  blssex  12588  mopni3  12642  metrest  12664  metcnp3  12669  mulc1cncf  12734  cncfco  12736  subctctexmid  13185
  Copyright terms: Public domain W3C validator