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

Theorem rexlimdv 2410
Description: Inference from Theorem 19.23 of [Margaris] p. 90 (restricted quantifier version). (Contributed by NM, 14-Nov-2002.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)
Hypothesis
Ref Expression
rexlimdv.1 (φ → (x A → (ψχ)))
Assertion
Ref Expression
rexlimdv (φ → (x A ψχ))
Distinct variable groups:   φ,x   χ,x
Allowed substitution hints:   ψ(x)   A(x)

Proof of Theorem rexlimdv
StepHypRef Expression
1 nfv 1402 . 2 xφ
2 nfv 1402 . 2 xχ
3 rexlimdv.1 . 2 (φ → (x A → (ψχ)))
41, 2, 3rexlimd 2408 1 (φ → (x A ψχ))
Colors of variables: wff set class
Syntax hints:  wi 4   wcel 1374  wrex 2285
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 1363  ax-ie2 1364  ax-4 1381  ax-17 1400  ax-ial 1409  ax-i5r 1410
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-ral 2289  df-rex 2290
This theorem is referenced by:  rexlimdva  2411  rexlimdv3a  2413  rexlimdvw  2414  rexlimdvv  2417  trintssm  3844  ssorduni  4163  funcnvuni  4894  dffo3  5239  smoiun  5838  tfrlem9  5857  axprecex  6574
  Copyright terms: Public domain W3C validator