Theorem spw 1967

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

Hypothesis

Ref	Expression
spw.1	⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
spw	⊢ (∀𝑥𝜑 → 𝜑)

Distinct variable groups:   𝑥,𝑦   𝜓,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem spw

Step	Hyp	Ref	Expression
1		ax-5 1839	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
2		ax-5 1839	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
3		ax-5 1839	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
4		spw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	spfw 1965	1 ⊢ (∀𝑥𝜑 → 𝜑)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196  ∀wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705

This theorem is referenced by:  hba1w  1974  hba1wOLD  1975  spaev  1978  ax12w  2010  bj-ssblem1  32630  bj-ax12w  32665