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

Theorem rexlimdva 2427
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 2426 1 (φ → (x A ψχ))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wcel 1390  wrex 2301
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 1333  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-i5r 1425
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305  df-rex 2306
This theorem is referenced by:  rexlimdvaa  2428  rexlimivv  2432  rexlimdvv  2433  ralxfrd  4159  rexxfrd  4160  fvelimab  5170  foco2  5259  elunirn  5346  f1elima  5353  tfrlem5  5868  tfrlemibacc  5878  tfrlemibfn  5880  nnaordex  6029  nnawordex  6030  ectocld  6101  ltexnqq  6384  ltbtwnnqq  6391  prarloclem4  6473  prarloc2  6479  genprndl  6497  genprndu  6498  prmuloc2  6538  1idprl  6556  1idpru  6557  recexgt0sr  6653  cnegexlem1  6935  cnegexlem2  6936  renegcl  7020  qmulz  8283  icc0r  8513  frec2uzrand  8818
  Copyright terms: Public domain W3C validator