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	⊢ ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 )
	spfw.2	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
	spfw.3	⊢ ( ¬ 𝜑 → ∀ 𝑦 ¬ 𝜑 )
	spfw.4	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
Assertion	spfw	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		spfw.1	⊢ ( ¬ 𝜓 → ∀ 𝑥 ¬ 𝜓 )
2		spfw.2	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 ∀ 𝑥 𝜑 )
3		spfw.3	⊢ ( ¬ 𝜑 → ∀ 𝑦 ¬ 𝜑 )
4		spfw.4	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
5	4	biimpd	⊢ ( 𝑥 = 𝑦 → ( 𝜑 → 𝜓 ) )
6	2 1 5	cbvaliw	⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑦 𝜓 )
7	4	biimprd	⊢ ( 𝑥 = 𝑦 → ( 𝜓 → 𝜑 ) )
8	7	equcoms	⊢ ( 𝑦 = 𝑥 → ( 𝜓 → 𝜑 ) )
9	3 8	spimw	⊢ ( ∀ 𝑦 𝜓 → 𝜑 )
10	6 9	syl	⊢ ( ∀ 𝑥 𝜑 → 𝜑 )