![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > spi | Structured version Visualization version GIF 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 2206 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1628 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1869 ax-4 1884 ax-5 1990 ax-6 2056 ax-7 2092 ax-12 2202 |
This theorem depends on definitions: df-bi 197 df-ex 1852 |
This theorem is referenced by: darii 2713 barbari 2715 cesare 2717 camestres 2718 festino 2719 baroco 2720 cesaro 2721 camestros 2722 datisi 2723 disamis 2724 felapton 2727 darapti 2728 calemes 2729 dimatis 2730 fresison 2731 calemos 2732 fesapo 2733 bamalip 2734 kmlem2 9174 axac2 9489 axac 9490 axaci 9491 bnj864 31324 |
Copyright terms: Public domain | W3C validator |