This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ψ \to \forall x \neg ψ$
	spfw.2	$⊢ \forall x φ \to \forall y \forall x φ$
	spfw.3	$⊢ \neg φ \to \forall y \neg φ$
	spfw.4	$⊢ x = y \to (φ \leftrightarrow ψ)$
Assertion	spfw	$⊢ \forall x φ \to φ$

Proof

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