Theorem spw 2123

Description: Weak version of the specialization scheme sp 2207. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 2207 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 2207 having mutually distinct setvar variables and no wff metavariables (see ax12wdemo 2167 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 2207 are spfw 2121 (minimal distinct variable requirements), spnfw 2086 (when 𝑥 is not free in ¬ 𝜑), spvw 2067 (when 𝑥 does not appear in 𝜑), sptruw 1881 (when 𝜑 is true), and spfalw 2087 (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 1991	. 2 ⊢ (¬ 𝜓 → ∀𝑥 ¬ 𝜓)
2		ax-5 1991	. 2 ⊢ (∀𝑥𝜑 → ∀𝑦∀𝑥𝜑)
3		ax-5 1991	. 2 ⊢ (¬ 𝜑 → ∀𝑦 ¬ 𝜑)
4		spw.1	. 2 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
5	1, 2, 3, 4	spfw 2121	1 ⊢ (∀𝑥𝜑 → 𝜑)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093

This theorem depends on definitions:  df-bi 197  df-an 383  df-ex 1853

This theorem is referenced by:  hba1w  2131  hba1wOLD  2132  spaev  2135  ax12w  2165  bj-ssblem1  32968  bj-ax12w  33002