Theorem spw 1694

Description: Weak version of specialization scheme sp 1747. Lemma 9 of [KalishMontague] p. 87. While it appears that sp 1747 in its general form does not follow from Tarski's FOL axiom schemes, from this theorem we can prove any instance of sp 1747 having no wff metavariables and mutually distinct setvar variables (see ax11wdemo 1723 for an example of the procedure to eliminate the hypothesis). Other approximations of sp 1747 are spfw 1691 (minimal distinct variable requirements), spnfw 1670 (when x is not free in ¬ φ), spvw 1666 (when x does not appear in φ), sptruw 1671 (when φ is true), and spfalw 1672 (when φ is false). (Contributed by NM, 9-Apr-2017.)

Hypothesis

Ref	Expression
spw.1	⊢ (x = y → (φ ↔ ψ))

Assertion

Ref	Expression
spw	⊢ (∀xφ → φ)

Distinct variable groups:   x,y   ψ,x   φ,y

Allowed substitution hints:   φ(x)   ψ(y)

Proof of Theorem spw

Step	Hyp	Ref	Expression
1		ax-17 1616	. . 3 ⊢ (∀xφ → ∀y∀xφ)
2		ax-5 1557	. . 3 ⊢ (∀y(∀xφ → ψ) → (∀y∀xφ → ∀yψ))
3		spw.1	. . . . . 6 ⊢ (x = y → (φ ↔ ψ))
4	3	biimprd 214	. . . . 5 ⊢ (x = y → (ψ → φ))
5	4	equcoms 1681	. . . 4 ⊢ (y = x → (ψ → φ))
6	5	spimvw 1669	. . 3 ⊢ (∀yψ → φ)
7	1, 2, 6	syl56 30	. 2 ⊢ (∀y(∀xφ → ψ) → (∀xφ → φ))
8	3	biimpd 198	. . 3 ⊢ (x = y → (φ → ψ))
9	8	spimvw 1669	. 2 ⊢ (∀xφ → ψ)
10	7, 9	mpg 1548	1 ⊢ (∀xφ → φ)

Syntax hints:   → wi 4   ↔ wb 176  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675

This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1542

This theorem is referenced by:  spvwOLD  1695  spfalwOLD  1699  hba1w  1707  ax11w  1721