Theorem ax4567to7 16363

Description: Re-derivation of ax-7 1304 from ax4567 16359. Note that ax-7 1304 is not required for the re-derivation.

Assertion

Ref	Expression
ax4567to7	|- (A.xA.yph -> A.yA.xph)

Proof of Theorem ax4567to7

Step	Hyp	Ref	Expression
1		ax-1 4	. . 3 |- (ph -> (A.y(ph -> ph) -> ph))
2	1	2alimi 1339	. 2 |- (A.xA.yph -> A.xA.y(A.y(ph -> ph) -> ph))
3		ax4567to6 16362	. . . 4 |- (-. A.y -. A.y -. A.xA.y(A.y(ph -> ph) -> ph) -> -. A.xA.y(A.y(ph -> ph) -> ph))
4	3	con4i 90	. . 3 |- (A.xA.y(A.y(ph -> ph) -> ph) -> A.y -. A.y -. A.xA.y(A.y(ph -> ph) -> ph))
5		pm2.21 92	. . . . . . 7 |- (-. A.xA.y -. A.xA.y(A.y(ph -> ph) -> ph) -> (A.xA.y -. A.xA.y(A.y(ph -> ph) -> ph) -> ((ph -> ph) -> A.y(A.y(ph -> ph) -> ph))))
6		ax4567 16359	. . . . . . . 8 |- ((A.xA.y -. A.xA.y(A.y(ph -> ph) -> ph) -> ((ph -> ph) -> A.y(A.y(ph -> ph) -> ph))) -> (A.y(ph -> ph) -> A.yph))
7		ax-4 1319	. . . . . . . 8 |- (A.yph -> ph)
8	6, 7	syl6 25	. . . . . . 7 |- ((A.xA.y -. A.xA.y(A.y(ph -> ph) -> ph) -> ((ph -> ph) -> A.y(A.y(ph -> ph) -> ph))) -> (A.y(ph -> ph) -> ph))
9	5, 8	syl 12	. . . . . 6 |- (-. A.xA.y -. A.xA.y(A.y(ph -> ph) -> ph) -> (A.y(ph -> ph) -> ph))
10	9	alimi 1338	. . . . 5 |- (A.x -. A.xA.y -. A.xA.y(A.y(ph -> ph) -> ph) -> A.x(A.y(ph -> ph) -> ph))
11		ax4567to6 16362	. . . . 5 |- (-. A.x -. A.xA.y -. A.xA.y(A.y(ph -> ph) -> ph) -> A.y -. A.xA.y(A.y(ph -> ph) -> ph))
12	10, 11	nsyl4 135	. . . 4 |- (-. A.y -. A.xA.y(A.y(ph -> ph) -> ph) -> A.x(A.y(ph -> ph) -> ph))
13	12	alimi 1338	. . 3 |- (A.y -. A.y -. A.xA.y(A.y(ph -> ph) -> ph) -> A.yA.x(A.y(ph -> ph) -> ph))
14	4, 13	syl 12	. 2 |- (A.xA.y(A.y(ph -> ph) -> ph) -> A.yA.x(A.y(ph -> ph) -> ph))
15		pm2.27 76	. . . 4 |- (A.y(ph -> ph) -> ((A.y(ph -> ph) -> ph) -> ph))
16		id 73	. . . 4 |- (ph -> ph)
17	15, 16	mpg 1332	. . 3 |- ((A.y(ph -> ph) -> ph) -> ph)
18	17	2alimi 1339	. 2 |- (A.yA.x(A.y(ph -> ph) -> ph) -> A.yA.xph)
19	2, 14, 18	3syl 24	1 |- (A.xA.yph -> A.yA.xph)

Syntax hints:  -. wn 2   -> wi 3  A.wal 1296

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-6 1303  ax-7 1304  ax-gen 1305  ax-4 1319  ax-5o 1321  ax-6o 1324

Copyright terms: Public domain