NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  spOLD GIF version

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.
StepHypRef Expression
1 ax9v 1655 . 2 ¬ w ¬ w = x
2 equcomi 1679 . . . . . . 7 (w = xx = w)
3 ax-17 1616 . . . . . . 7 φw ¬ φ)
4 ax-11 1746 . . . . . . 7 (x = w → (w ¬ φx(x = w → ¬ φ)))
52, 3, 4syl2im 34 . . . . . 6 (w = x → (¬ φx(x = w → ¬ φ)))
6 ax9v 1655 . . . . . . 7 ¬ x ¬ x = w
7 con2 108 . . . . . . . 8 ((x = w → ¬ φ) → (φ → ¬ x = w))
87al2imi 1561 . . . . . . 7 (x(x = w → ¬ φ) → (xφx ¬ x = w))
96, 8mtoi 169 . . . . . 6 (x(x = w → ¬ φ) → ¬ xφ)
105, 9syl6 29 . . . . 5 (w = x → (¬ φ → ¬ xφ))
1110con4d 97 . . . 4 (w = x → (xφφ))
1211con3i 127 . . 3 (¬ (xφφ) → ¬ w = x)
1312alrimiv 1631 . 2 (¬ (xφφ) → w ¬ w = x)
141, 13mt3 171 1 (xφφ)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  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  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator