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

Theorem rexlimdvva 2440
 Description: Inference from Theorem 19.23 of [Margaris] p. 90. (Restricted quantifier version.) (Contributed by NM, 18-Jun-2014.)
Hypothesis
Ref Expression
rexlimdvva.1
Assertion
Ref Expression
rexlimdvva
Distinct variable groups:   ,,   ,,   ,
Allowed substitution hints:   (,)   ()   (,)

Proof of Theorem rexlimdvva
StepHypRef Expression
1 rexlimdvva.1 . . 3
21ex 108 . 2
32rexlimdvv 2439 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 97   wcel 1393  wrex 2307 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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2311  df-rex 2312 This theorem is referenced by:  ovelrn  5649  f1o2ndf1  5849  eroveu  6197  eroprf  6199  genipv  6607  genpelvl  6610  genpelvu  6611  genprndl  6619  genprndu  6620  addlocpr  6634  addnqprlemrl  6655  addnqprlemru  6656  mulnqprlemrl  6671  mulnqprlemru  6672  ltsopr  6694  ltaddpr  6695  ltexprlemfl  6707  ltexprlemrl  6708  ltexprlemfu  6709  ltexprlemru  6710  cauappcvgprlemladdfu  6752  cauappcvgprlemladdfl  6753  caucvgprlemdisj  6772  caucvgprlemladdfu  6775  caucvgprprlemdisj  6800  apreap  7578  apreim  7594  apirr  7596  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  apti  7613  qapne  8574  qtri3or  9098  qbtwnzlemex  9105  rebtwn2z  9109  cjap  9506  climcn2  9830
 Copyright terms: Public domain W3C validator