![]() |
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 143 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | spimv 1763 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1404 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 |
This theorem depends on definitions: df-bi 116 df-nf 1418 |
This theorem is referenced by: chvarv 1885 ru 2875 nalset 4016 tfisi 4459 tfr1onlemsucfn 6189 tfr1onlemsucaccv 6190 tfr1onlembxssdm 6192 tfr1onlembfn 6193 tfr1onlemres 6198 tfri1dALT 6200 tfrcllemsucfn 6202 tfrcllemsucaccv 6203 tfrcllembxssdm 6205 tfrcllembfn 6206 tfrcllemres 6211 findcard2 6734 findcard2s 6735 bj-nalset 12776 |
Copyright terms: Public domain | W3C validator |