![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > spi | Structured version Visualization version GIF version |
Description: Inference rule of universal instantiation, or universal specialization. Converse of the inference rule of (universal) generalization ax-gen 1839. Contrary to the rule of generalization, its closed form is valid, see sp 2166. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
spi.1 | ⊢ ∀𝑥𝜑 |
Ref | Expression |
---|---|
spi | ⊢ 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | spi.1 | . 2 ⊢ ∀𝑥𝜑 | |
2 | sp 2166 | . 2 ⊢ (∀𝑥𝜑 → 𝜑) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝜑 |
Colors of variables: wff setvar class |
Syntax hints: ∀wal 1599 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2054 ax-12 2162 |
This theorem depends on definitions: df-bi 199 df-ex 1824 |
This theorem is referenced by: dariiALT 2697 barbariALT 2701 cesareOLD 2704 camestresOLD 2706 festinoALT 2708 barocoALT 2710 cesaroOLD 2712 camestrosOLD 2714 datisiOLD 2716 disamisOLD 2718 daraptiALT 2722 calemesOLD 2725 dimatisOLD 2727 fresisonOLD 2729 calemosOLD 2731 fesapoOLD 2733 bamalipOLD 2735 kmlem2 9308 axac2 9623 axac 9624 axaci 9625 bnj864 31591 |
Copyright terms: Public domain | W3C validator |