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

Theorem exlimdv 1678
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 (φ → (xψχ))
Distinct variable groups:   χ,x   φ,x
Allowed substitution hint:   ψ(x)

Proof of Theorem exlimdv
StepHypRef Expression
1 ax-17 1396 . 2 (φxφ)
2 ax-17 1396 . 2 (χxχ)
3 exlimdv.1 . 2 (φ → (ψχ))
41, 2, 3exlimdh 1465 1 (φ → (xψχ))
Colors of variables: wff set class
Syntax hints:  wi 4  wex 1358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-5 1312  ax-gen 1314  ax-ie2 1360  ax-17 1396
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  ax11v2  1679  exlimdvv  1755  exlimddv  1756  tpid3g  3453  sssnm  3495  euotd  3961  ralxfr2d  4142  rexxfr2d  4143  releldmb  4494  relelrnb  4495  elres  4569  iss  4577  imain  4903  elunirn  5326  ovmpt4g  5542  op1steq  5724  fo2ndf  5767  reldmtpos  5786  rntpos  5790  tfrlemibacc  5857  tfrlemibxssdm  5858  tfrlemibfn  5859  tfrexlem  5866  recclnq  6245  ltexnqq  6260  ltbtwnnqq  6266  recexprlemss1l  6463  recexprlemss1u  6464
  Copyright terms: Public domain W3C validator