Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sp | GIF version |
Description: Specialization. Another name for ax-4 1400. (Contributed by NM, 21-May-2008.) |
Ref | Expression |
---|---|
sp | ⊢ (∀𝑥𝜑 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-4 1400 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1241 |
This theorem was proved from axioms: ax-4 1400 |
This theorem is referenced by: axi12 1407 nfr 1411 sps 1430 spsd 1431 19.3 1446 cbv1h 1633 nfald 1643 dveeq2 1696 nfsbxy 1818 nfsbxyt 1819 nfcr 2170 rsp 2369 ceqex 2671 abidnf 2709 mob2 2721 csbie2t 2894 sbcnestgf 2897 mpteq12f 3837 dtruarb 3942 copsex2t 3982 ssopab2 4012 eusv1 4184 alxfr 4193 eunex 4285 iota1 4881 genprndl 6619 genprndu 6620 bdel 9965 bdsepnft 10007 strcollnft 10109 |
Copyright terms: Public domain | W3C validator |