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

Theorem reximdv 2414
Description: Deduction from Theorem 19.22 of [Margaris] p. 90. (Restricted quantifier version with strong hypothesis.) (Contributed by NM, 24-Jun-1998.)
Hypothesis
Ref Expression
reximdv.1
Assertion
Ref Expression
reximdv
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem reximdv
StepHypRef Expression
1 reximdv.1 . . 3
21a1d 22 . 2
32reximdvai 2413 1
Colors of variables: wff set class
Syntax hints:   wi 4   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:  r19.12  2416  reusv3  4158  rexxfrd  4161  iunpw  4177  fvelima  5168  prnmaddl  6473  prarloclem5  6483  prarloc2  6487  genprndl  6504  genprndu  6505  ltpopr  6569  recexprlemm  6596  recexprlemopl  6597  recexprlemopu  6599  recexprlem1ssl  6605  recexprlem1ssu  6606  cauappcvgprlemupu  6621  caucvgprlemupu  6643
  Copyright terms: Public domain W3C validator