![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sp | GIF version |
Description: Specialization. Another name for ax-4 1455. (Contributed by NM, 21-May-2008.) |
Ref | Expression |
---|---|
sp | ⊢ (∀𝑥𝜑 → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-4 1455 | 1 ⊢ (∀𝑥𝜑 → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∀wal 1297 |
This theorem was proved from axioms: ax-4 1455 |
This theorem is referenced by: axi12 1462 nfr 1466 sps 1485 spsd 1486 19.3 1501 cbv1h 1691 nfald 1701 dveeq2 1754 nfsbxy 1878 nfsbxyt 1879 nfcr 2232 rsp 2439 ceqex 2766 abidnf 2805 mob2 2817 csbie2t 2998 sbcnestgf 3001 mpteq12f 3948 dtruarb 4055 copsex2t 4105 ssopab2 4135 eusv1 4311 alxfr 4320 eunex 4414 iota1 5038 fiintim 6746 genprndl 7230 genprndu 7231 fiinopn 11953 bdel 12624 bdsepnft 12666 strcollnft 12767 |
Copyright terms: Public domain | W3C validator |