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  6492  genpelvl  6495  genpelvu  6496  genprndl  6504  genprndu  6505  addlocpr  6519  addnqprlemrl  6538  addnqprlemru  6539  ltsopr  6570  ltaddpr  6571  ltexprlemfl  6583  ltexprlemrl  6584  ltexprlemfu  6585  ltexprlemru  6586  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemdisj  6645  caucvgprlemladdfu  6648  apreap  7371  apreim  7387  apirr  7389  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  apti  7406  qapne  8350  cjap  9134
  Copyright terms: Public domain W3C validator