Theorem spOLD 1748

Description: Obsolete proof of sp 1747 as of 23-Dec-2017. (Contributed by NM, 21-May-2008.) (Proof shortened by Scott Fenton, 24-Jan-2011.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
spOLD	⊢ (∀xφ → φ)

Proof of Theorem spOLD

Dummy variable w is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax9v 1655	. 2 ⊢ ¬ ∀w ¬ w = x
2		equcomi 1679	. . . . . . 7 ⊢ (w = x → x = w)
3		ax-17 1616	. . . . . . 7 ⊢ (¬ φ → ∀w ¬ φ)
4		ax-11 1746	. . . . . . 7 ⊢ (x = w → (∀w ¬ φ → ∀x(x = w → ¬ φ)))
5	2, 3, 4	syl2im 34	. . . . . 6 ⊢ (w = x → (¬ φ → ∀x(x = w → ¬ φ)))
6		ax9v 1655	. . . . . . 7 ⊢ ¬ ∀x ¬ x = w
7		con2 108	. . . . . . . 8 ⊢ ((x = w → ¬ φ) → (φ → ¬ x = w))
8	7	al2imi 1561	. . . . . . 7 ⊢ (∀x(x = w → ¬ φ) → (∀xφ → ∀x ¬ x = w))
9	6, 8	mtoi 169	. . . . . 6 ⊢ (∀x(x = w → ¬ φ) → ¬ ∀xφ)
10	5, 9	syl6 29	. . . . 5 ⊢ (w = x → (¬ φ → ¬ ∀xφ))
11	10	con4d 97	. . . 4 ⊢ (w = x → (∀xφ → φ))
12	11	con3i 127	. . 3 ⊢ (¬ (∀xφ → φ) → ¬ w = x)
13	12	alrimiv 1631	. 2 ⊢ (¬ (∀xφ → φ) → ∀w ¬ w = x)
14	1, 13	mt3 171	1 ⊢ (∀xφ → φ)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4  ∀wal 1540

This proof depends on 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  ax-11 1746

This proof depends on definitions:  df-bi 177  df-ex 1542

This theorem is used by: (None)