Theorem spfw

Description: Weak version of sp . Uses only Tarski's FOL axiom schemes. Lemma 9 of KalishMontague p. 87. This may be the best we can do with minimal distinct variable conditions. (Contributed by NM, 19-Apr-2017) (Proof shortened by Wolf Lammen, 10-Oct-2021)

	Ref	Expression
Hypotheses	spfw.1	$$⊢\neg \psi \to \forall x\neg \psi$$
	spfw.2	$$⊢\forall x\phi \to \forall y\forall x\phi$$
	spfw.3	$$⊢\neg \phi \to \forall y\neg \phi$$
	spfw.4	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	spfw	$$⊢\forall x\phi \to \phi$$

Proof

Step	Hyp	Ref	Expression
1		spfw.1	$$⊢\neg \psi \to \forall x\neg \psi$$
2		spfw.2	$$⊢\forall x\phi \to \forall y\forall x\phi$$
3		spfw.3	$$⊢\neg \phi \to \forall y\neg \phi$$
4		spfw.4	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
5	4	biimpd	$$⊢x=y\to \left(\phi \to \psi \right)$$
6	2 1 5	cbvaliw	$$⊢\forall x\phi \to \forall y\psi$$
7	4	biimprd	$$⊢x=y\to \left(\psi \to \phi \right)$$
8	7	equcoms	$$⊢y=x\to \left(\psi \to \phi \right)$$
9	3 8	spimw	$$⊢\forall y\psi \to \phi$$
10	6 9	syl	$$⊢\forall x\phi \to \phi$$