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

Theorem rexlimdvva 2434
Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvva.1 ((φ (x A y B)) → (ψχ))
Assertion
Ref Expression
rexlimdvva (φ → (x A y B ψχ))
Distinct variable groups:   x,y,φ   χ,x,y   y,A
Allowed substitution hints:   ψ(x,y)   A(x)   B(x,y)

Proof of Theorem rexlimdvva
StepHypRef Expression
1 rexlimdvva.1 . . 3 ((φ (x A y B)) → (ψχ))
21ex 108 . 2 (φ → ((x A y B) → (ψχ)))
32rexlimdvv 2433 1 (φ → (x A y B ψχ))
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:  ovelrn  5591  f1o2ndf1  5791  eroveu  6133  eroprf  6135  genipv  6491  genpelvl  6494  genpelvu  6495  genprndl  6504  genprndu  6505  addlocpr  6519  addnqpr1lemrl  6537  addnqpr1lemru  6538  ltsopr  6568  ltaddpr  6569  ltexprlemfl  6581  ltexprlemrl  6582  ltexprlemfu  6583  ltexprlemru  6584  apreap  7331  apreim  7347  apirr  7349  apsym  7350  apcotr  7351  apadd1  7352  apneg  7355  mulext1  7356  apti  7366  qapne  8310  cjap  9094
  Copyright terms: Public domain W3C validator