Theorem ax16i 1846

Description: Inference with ax-16 1802 as its conclusion, that does not require ax-10 1493, ax-11 1494, or ax12 1500 for its proof. The hypotheses may be eliminable without one or more of these axioms in special cases. (Contributed by NM, 20-May-2008.)

Hypotheses

Ref	Expression
ax16i.1	|- ( x = z -> ( ph <-> ps ) )
ax16i.2	|- ( ps -> A. x ps )

Assertion

Ref	Expression
ax16i	|- ( A. x x = y -> ( ph -> A. x ph ) )

Distinct variable groups:   x, y, z   ph, z

Allowed substitution hints:   ph( x, y)   ps( x, y, z)

Proof of Theorem ax16i

Step	Hyp	Ref	Expression
1		ax-17 1514	. . . 4 |- ( x = y -> A. z x = y )
2		ax-17 1514	. . . 4 |- ( z = y -> A. x z = y )
3		ax-8 1492	. . . 4 |- ( x = z -> ( x = y -> z = y ) )
4	1, 2, 3	cbv3h 1731	. . 3 |- ( A. x x = y -> A. z z = y )
5		ax-8 1492	. . . . . 6 |- ( z = x -> ( z = y -> x = y ) )
6	5	spimv 1799	. . . . 5 |- ( A. z z = y -> x = y )
7		equid 1689	. . . . . . . 8 |- x = x
8		ax-8 1492	. . . . . . . 8 |- ( x = y -> ( x = x -> y = x ) )
9	7, 8	mpi 15	. . . . . . 7 |- ( x = y -> y = x )
10		equid 1689	. . . . . . . . 9 |- z = z
11		ax-8 1492	. . . . . . . . 9 |- ( z = y -> ( z = z -> y = z ) )
12	10, 11	mpi 15	. . . . . . . 8 |- ( z = y -> y = z )
13		ax-8 1492	. . . . . . . 8 |- ( y = z -> ( y = x -> z = x ) )
14	12, 13	syl 14	. . . . . . 7 |- ( z = y -> ( y = x -> z = x ) )
15	9, 14	syl5com 29	. . . . . 6 |- ( x = y -> ( z = y -> z = x ) )
16	1, 15	alimdh 1455	. . . . 5 |- ( x = y -> ( A. z z = y -> A. z z = x ) )
17	6, 16	mpcom 36	. . . 4 |- ( A. z z = y -> A. z z = x )
18		ax-8 1492	. . . . . 6 |- ( z = x -> ( z = z -> x = z ) )
19	10, 18	mpi 15	. . . . 5 |- ( z = x -> x = z )
20	19	alimi 1443	. . . 4 |- ( A. z z = x -> A. z x = z )
21	17, 20	syl 14	. . 3 |- ( A. z z = y -> A. z x = z )
22	4, 21	syl 14	. 2 |- ( A. x x = y -> A. z x = z )
23		ax-17 1514	. . . 4 |- ( ph -> A. z ph )
24		ax16i.1	. . . . 5 |- ( x = z -> ( ph <-> ps ) )
25	24	biimpcd 158	. . . 4 |- ( ph -> ( x = z -> ps ) )
26	23, 25	alimdh 1455	. . 3 |- ( ph -> ( A. z x = z -> A. z ps ) )
27		ax16i.2	. . . 4 |- ( ps -> A. x ps )
28	24	biimprd 157	. . . . 5 |- ( x = z -> ( ps -> ph ) )
29	19, 28	syl 14	. . . 4 |- ( z = x -> ( ps -> ph ) )
30	27, 23, 29	cbv3h 1731	. . 3 |- ( A. z ps -> A. x ph )
31	26, 30	syl6com 35	. 2 |- ( A. z x = z -> ( ph -> A. x ph ) )
32	22, 31	syl 14	1 |- ( A. x x = y -> ( ph -> A. x ph ) )

Syntax hints:   -> wi 4   <-> wb 104   A.wal 1341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449

This theorem is referenced by:  ax16ALT  1847