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

Theorem exlimdv 1697
Description: Deduction from Theorem 19.23 of [Margaris] p. 90. (Contributed by NM, 27-Apr-1994.)
Hypothesis
Ref Expression
exlimdv.1
Assertion
Ref Expression
exlimdv
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem exlimdv
StepHypRef Expression
1 ax-17 1416 . 2
2 ax-17 1416 . 2
3 exlimdv.1 . 2
41, 2, 3exlimdh 1484 1
Colors of variables: wff set class
Syntax hints:   wi 4  wex 1378
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-5 1333  ax-gen 1335  ax-ie2 1380  ax-17 1416
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11v2  1698  exlimdvv  1774  exlimddv  1775  tpid3g  3474  sssnm  3516  euotd  3982  ralxfr2d  4162  rexxfr2d  4163  releldmb  4514  relelrnb  4515  elres  4589  iss  4597  imain  4924  elunirn  5348  ovmpt4g  5565  op1steq  5747  fo2ndf  5790  reldmtpos  5809  rntpos  5813  tfrlemibacc  5881  tfrlemibxssdm  5882  tfrlemibfn  5883  tfrexlem  5889  freccl  5932  xpdom3m  6244  recclnq  6376  ltexnqq  6391  ltbtwnnqq  6398  recexprlemss1l  6607  recexprlemss1u  6608  negm  8326
  Copyright terms: Public domain W3C validator