Theorem ax4567to4 17184

Description: Re-derivation of ax-4 1608 from ax4567 17183. Note that ax-9 1595 is used for the re-derivation.

Assertion

Ref	Expression
ax4567to4	|- (A.xph -> ph)

Proof of Theorem ax4567to4

Step	Hyp	Ref	Expression
1		ax-9 1595	. . 3 |- -. A.x -. x = y
2		pm2.21 124	. . . . 5 |- (-. ph -> (ph -> A.x(A.xph -> -. x = y)))
3		ax-1 4	. . . . . 6 |- ((ph -> A.x(A.xph -> -. x = y)) -> (A.xA.x -. A.xA.x(A.xph -> -. x = y) -> (ph -> A.x(A.xph -> -. x = y))))
4		ax4567 17183	. . . . . 6 |- ((A.xA.x -. A.xA.x(A.xph -> -. x = y) -> (ph -> A.x(A.xph -> -. x = y))) -> (A.xph -> A.x -. x = y))
5	3, 4	syl 13	. . . . 5 |- ((ph -> A.x(A.xph -> -. x = y)) -> (A.xph -> A.x -. x = y))
6	2, 5	syl 13	. . . 4 |- (-. ph -> (A.xph -> A.x -. x = y))
7	6	con3d 145	. . 3 |- (-. ph -> (-. A.x -. x = y -> -. A.xph))
8	1, 7	mpi 97	. 2 |- (-. ph -> -. A.xph)
9	8	con4i 121	1 |- (A.xph -> ph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 1584   = wceq 1586

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-6 1591  ax-7 1592  ax-gen 1593  ax-9 1595  ax-4 1608  ax-5o 1610  ax-6o 1613

Copyright terms: Public domain