Theorem ax4567 16359

Description: Proof of a theorem that can act as a sole axiom for pure predicate calculus with ax-gen 1305 as the inference rule. This proof extends the idea of ax467 1370 and related theorems.

Assertion

Ref	Expression
ax4567	|- ((A.xA.y -. A.xA.y(A.yph -> ps) -> (ph -> A.y(A.yph -> ps))) -> (A.yph -> A.yps))

Proof of Theorem ax4567

Step	Hyp	Ref	Expression
1		ax-6 1303	. . . . 5 |- (-. A.y(A.yph -> ps) -> A.y -. A.y(A.yph -> ps))
2		ax-6o 1324	. . . . . . 7 |- (-. A.x -. A.xA.y(A.yph -> ps) -> A.y(A.yph -> ps))
3	2	con1i 112	. . . . . 6 |- (-. A.y(A.yph -> ps) -> A.x -. A.xA.y(A.yph -> ps))
4	3	alimi 1338	. . . . 5 |- (A.y -. A.y(A.yph -> ps) -> A.yA.x -. A.xA.y(A.yph -> ps))
5		ax-7 1304	. . . . 5 |- (A.yA.x -. A.xA.y(A.yph -> ps) -> A.xA.y -. A.xA.y(A.yph -> ps))
6	1, 4, 5	3syl 24	. . . 4 |- (-. A.y(A.yph -> ps) -> A.xA.y -. A.xA.y(A.yph -> ps))
7	6	con1i 112	. . 3 |- (-. A.xA.y -. A.xA.y(A.yph -> ps) -> A.y(A.yph -> ps))
8		ax-5o 1321	. . 3 |- (A.y(A.yph -> ps) -> (A.yph -> A.yps))
9	7, 8	syl 12	. 2 |- (-. A.xA.y -. A.xA.y(A.yph -> ps) -> (A.yph -> A.yps))
10		pm2.21 92	. . . 4 |- (-. ph -> (ph -> A.yps))
11	10	a4sd 1331	. . 3 |- (-. ph -> (A.yph -> A.yps))
12	11, 8	ja 152	. 2 |- ((ph -> A.y(A.yph -> ps)) -> (A.yph -> A.yps))
13	9, 12	ja 152	1 |- ((A.xA.y -. A.xA.y(A.yph -> ps) -> (ph -> A.y(A.yph -> ps))) -> (A.yph -> A.yps))

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

This theorem is referenced by:  ax4567to4 16360  ax4567to5 16361  ax4567to6 16362  ax4567to7 16363

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