Specialization (intuitionistic logic axiom ax-4). This is just sp by another name. (Contributed by Jim Kingdon, 31-Dec-2017.) (New usage is discouraged.)