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

Theorem exlimdv 1773
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
exlimdv.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
exlimdv  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Distinct variable groups:    ch, x    ph, x
Allowed substitution hint:    ps( x)

Proof of Theorem exlimdv
StepHypRef Expression
1 ax-17 1489 . 2  |-  ( ph  ->  A. x ph )
2 ax-17 1489 . 2  |-  ( ch 
->  A. x ch )
3 exlimdv.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
41, 2, 3exlimdh 1558 1  |-  ( ph  ->  ( E. x ps 
->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4   E.wex 1451
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-5 1406  ax-gen 1408  ax-ie2 1453  ax-17 1489
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax11v2  1774  exlimdvv  1851  exlimddv  1852  tpid3g  3606  sssnm  3649  pwntru  4090  euotd  4144  ralxfr2d  4353  rexxfr2d  4354  releldmb  4744  relelrnb  4745  elres  4823  iss  4833  imain  5173  elunirn  5633  ovmpt4g  5859  oprssdmm  6035  op1steq  6043  fo2ndf  6090  reldmtpos  6116  rntpos  6120  tfrlemibacc  6189  tfrlemibxssdm  6190  tfrlemibfn  6191  tfrexlem  6197  tfr1onlembacc  6205  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfrcllembacc  6218  tfrcllembxssdm  6219  tfrcllembfn  6220  map0g  6548  xpdom3m  6694  phplem4  6715  phpm  6725  findcard2  6749  findcard2s  6750  ac6sfi  6758  fiintim  6783  xpfi  6784  fidcenum  6810  ordiso  6887  ctmlemr  6959  ctm  6960  ctssdc  6964  pm54.43  7012  exmidfodomrlemim  7021  recclnq  7164  ltexnqq  7180  ltbtwnnqq  7187  recexprlemss1l  7407  recexprlemss1u  7408  negm  9359  ioom  9989  seq3f1olemp  10226  fiinfnf1o  10483  fihashf1rn  10486  climcau  11067  summodclem2  11102  zsumdc  11104  isumz  11109  fsumf1o  11110  fisumss  11112  fsumcl2lem  11118  fsumadd  11126  fsummulc2  11168  ennnfone  11844  enctlem  11851  unct  11860  eltg3  12132  tgtop  12143  tgidm  12149  tgrest  12244  tgcn  12283  xblm  12492  dvfgg  12732  dvcnp2cntop  12738  pwtrufal  13026
  Copyright terms: Public domain W3C validator