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

Theorem rexlimdva 2410
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 20-Jan-2007.)
Hypothesis
Ref Expression
rexlimdva.1 ((φ x A) → (ψχ))
Assertion
Ref Expression
rexlimdva (φ → (x A ψχ))
Distinct variable groups:   φ,x   χ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem rexlimdva
StepHypRef Expression
1 rexlimdva.1 . . 3 ((φ x A) → (ψχ))
21ex 108 . 2 (φ → (x A → (ψχ)))
32rexlimdv 2409 1 (φ → (x A ψχ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1375  wrex 2284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ie1 1364  ax-ie2 1365  ax-4 1382  ax-17 1401  ax-ial 1410  ax-i5r 1411
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-ral 2288  df-rex 2289
This theorem is referenced by:  rexlimdvaa  2411  rexlimivv  2415  rexlimdvv  2416  ralxfrd  4142  rexxfrd  4143  fvelimab  5152  foco2  5241  elunirn  5328  f1elima  5335  tfrlem5  5847  tfrlemibacc  5856  tfrlemibfn  5858  nnaordex  6006  nnawordex  6007  ectocld  6076  ltexnqq  6253  ltbtwnnqq  6259  prarloclem4  6335  genprndl  6353
  Copyright terms: Public domain W3C validator