![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sp | GIF version |
Description: Specialization. Another name for ax-4 1521. (Contributed by NM, 21-May-2008.) |
Ref | Expression |
---|---|
sp | ⊢ (∀𝑥𝜑 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-4 1521 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1362 |
This theorem was proved from axioms: ax-4 1521 |
This theorem is referenced by: axi12 1525 nfr 1529 sps 1548 spsd 1549 19.3 1565 cbv1h 1757 nfald 1771 dveeq2 1826 nfsbxy 1954 nfsbxyt 1955 nfcr 2324 nfabdw 2351 rsp 2537 ceqex 2879 abidnf 2920 mob2 2932 csbie2t 3120 sbcnestgf 3123 mpteq12f 4098 dtruarb 4209 copsex2t 4263 ssopab2 4293 eusv1 4470 alxfr 4479 eunex 4578 iota1 5210 fiintim 6958 genprndl 7551 genprndu 7552 fiinopn 13981 bdel 15075 bdsepnft 15117 strcollnft 15214 |
Copyright terms: Public domain | W3C validator |