Description: Weak version of the specialization scheme sp . Lemma 9 of
KalishMontague p. 87. While it appears that sp in its general form
does not follow from Tarski's FOL axiom schemes, from this theorem we
can prove anyinstance of sp having mutually distinct setvar
variables and no wff metavariables (see ax12wdemo for an example of
the procedure to eliminate the hypothesis). Other approximations of
sp are spfw (minimal distinct variable requirements), spnfw (when
x is not free in -. ph ), spvw (when x does not appear in
ph ), sptruw (when ph is true), spfalw (when ph is
false), and spvv (where ph is changed into ps ). (Contributed by NM, 9-Apr-2017)(Proof shortened by Wolf Lammen, 27-Feb-2018)