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

Theorem reximdva 2415
Description: Deduction quantifying both antecedent and consequent, based on Theorem 19.22 of [Margaris] p. 90. (Contributed by NM, 22-May-1999.)
Hypothesis
Ref Expression
reximdva.1
Assertion
Ref Expression
reximdva
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem reximdva
StepHypRef Expression
1 reximdva.1 . . 3
21ex 108 . 2
32reximdvai 2413 1
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
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305  df-rex 2306
This theorem is referenced by:  dffo4  5258  prarloclemarch  6401  appdivnq  6544  ltexprlemm  6574  ltexprlemopl  6575  ltexprlemopu  6577  ltexprlemloc  6581  archpr  6615  cauappcvgprlemm  6617  cauappcvgprlemopl  6618  cauappcvgprlemlol  6619  cauappcvgprlemopu  6620  cauappcvgprlemladdfu  6626  cauappcvgprlemladdfl  6627  caucvgprlemm  6639  caucvgprlemopl  6640  caucvgprlemlol  6641  caucvgprlemopu  6642  caucvgprlemladdfu  6648  caucvgprlemlim  6652  archsr  6708  cnegexlem2  6984  bndndx  7956  expnbnd  9025  expnlbnd2  9027
  Copyright terms: Public domain W3C validator