Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > spi | GIF 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 1490 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff set class |
Syntax hints: ∀wal 1333 |
This theorem was proved from axioms: ax-mp 5 ax-4 1490 |
This theorem is referenced by: 19.8a 1570 hbe1a 2003 darii 2106 barbari 2108 cesare 2110 camestres 2111 festino 2112 baroco 2113 cesaro 2114 camestros 2115 datisi 2116 disamis 2117 felapton 2120 darapti 2121 calemes 2122 dimatis 2123 fresison 2124 calemos 2125 fesapo 2126 bamalip 2127 tfi 4541 acexmid 5823 bdsep1 13471 strcoll2 13569 sscoll2 13574 |
Copyright terms: Public domain | W3C validator |