Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > spi | Unicode version |
Description: Inference reversing generalization (specialization). (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
spi.1 |
Ref | Expression |
---|---|
spi |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spi.1 | . 2 | |
2 | ax-4 1472 | . 2 | |
3 | 1, 2 | ax-mp 5 | 1 |
Colors of variables: wff set class |
Syntax hints: wal 1314 |
This theorem was proved from axioms: ax-mp 5 ax-4 1472 |
This theorem is referenced by: 19.8a 1554 darii 2077 barbari 2079 cesare 2081 camestres 2082 festino 2083 baroco 2084 cesaro 2085 camestros 2086 datisi 2087 disamis 2088 felapton 2091 darapti 2092 calemes 2093 dimatis 2094 fresison 2095 calemos 2096 fesapo 2097 bamalip 2098 tfi 4466 acexmid 5741 bdsep1 13010 strcoll2 13108 sscoll2 13113 |
Copyright terms: Public domain | W3C validator |