![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > spv | Unicode version |
Description: Specialization, using implicit substitition. (Contributed by NM, 30-Aug-1993.) |
Ref | Expression |
---|---|
spv.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
spv |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spv.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | biimpd 144 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | spimv 1822 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 |
This theorem depends on definitions: df-bi 117 df-nf 1472 |
This theorem is referenced by: spvv 1919 cbvalvw 1931 chvarv 1949 ru 2976 nalset 4148 tfisi 4604 tfr1onlemsucfn 6366 tfr1onlemsucaccv 6367 tfr1onlembxssdm 6369 tfr1onlembfn 6370 tfr1onlemres 6375 tfri1dALT 6377 tfrcllemsucfn 6379 tfrcllemsucaccv 6380 tfrcllembxssdm 6382 tfrcllembfn 6383 tfrcllemres 6388 findcard2 6918 findcard2s 6919 bj-nalset 15125 |
Copyright terms: Public domain | W3C validator |