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 1767 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 wal 1314 |
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 1408 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 |
This theorem depends on definitions: df-bi 116 df-nf 1422 |
This theorem is referenced by: chvarv 1889 ru 2881 nalset 4028 tfisi 4471 tfr1onlemsucfn 6205 tfr1onlemsucaccv 6206 tfr1onlembxssdm 6208 tfr1onlembfn 6209 tfr1onlemres 6214 tfri1dALT 6216 tfrcllemsucfn 6218 tfrcllemsucaccv 6219 tfrcllembxssdm 6221 tfrcllembfn 6222 tfrcllemres 6227 findcard2 6751 findcard2s 6752 bj-nalset 13020 |
Copyright terms: Public domain | W3C validator |