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

Theorem spv 1833
 Description: Specialization, using implicit substitition. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
spv.1
Assertion
Ref Expression
spv
Distinct variable group:   ,
Allowed substitution hints:   (,)   ()

Proof of Theorem spv
StepHypRef Expression
1 spv.1 . . 3
21biimpd 143 . 2
32spimv 1784 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104  wal 1330 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515 This theorem depends on definitions:  df-bi 116  df-nf 1438 This theorem is referenced by:  spvv  1880  chvarv  1910  ru  2911  nalset  4065  tfisi  4508  tfr1onlemsucfn  6244  tfr1onlemsucaccv  6245  tfr1onlembxssdm  6247  tfr1onlembfn  6248  tfr1onlemres  6253  tfri1dALT  6255  tfrcllemsucfn  6257  tfrcllemsucaccv  6258  tfrcllembxssdm  6260  tfrcllembfn  6261  tfrcllemres  6266  findcard2  6790  findcard2s  6791  bj-nalset  13262
 Copyright terms: Public domain W3C validator