![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > spi | Unicode version |
Description: Inference rule reversing generalization. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
spi.1 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
spi |
![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spi.1 |
. 2
![]() ![]() ![]() ![]() | |
2 | sp 1759 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 8 |
1
![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem is referenced by: darii 2361 barbari 2363 cesare 2365 camestres 2366 festino 2367 baroco 2368 cesaro 2369 camestros 2370 datisi 2371 disamis 2372 felapton 2375 darapti 2376 calemes 2377 dimatis 2378 fresison 2379 calemos 2380 fesapo 2381 bamalip 2382 kmlem2 7995 axac2 8310 axac 8311 axaci 8312 bnj864 29011 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-11 1757 |
This theorem depends on definitions: df-bi 178 df-ex 1548 |
Copyright terms: Public domain | W3C validator |