Theorem ax16i 1872

Description: Inference with ax-16 1828 as its conclusion, that does not require ax-10 1519, ax-11 1520, or ax12 1526 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 1540	. . . 4 |- ( x = y -> A. z x = y )
2		ax-17 1540	. . . 4 |- ( z = y -> A. x z = y )
3		ax-8 1518	. . . 4 |- ( x = z -> ( x = y -> z = y ) )
4	1, 2, 3	cbv3h 1757	. . 3 |- ( A. x x = y -> A. z z = y )
5		ax-8 1518	. . . . . 6 |- ( z = x -> ( z = y -> x = y ) )
6	5	spimv 1825	. . . . 5 |- ( A. z z = y -> x = y )
7		equid 1715	. . . . . . . 8 |- x = x
8		ax-8 1518	. . . . . . . 8 |- ( x = y -> ( x = x -> y = x ) )
9	7, 8	mpi 15	. . . . . . 7 |- ( x = y -> y = x )
10		equid 1715	. . . . . . . . 9 |- z = z
11		ax-8 1518	. . . . . . . . 9 |- ( z = y -> ( z = z -> y = z ) )
12	10, 11	mpi 15	. . . . . . . 8 |- ( z = y -> y = z )
13		ax-8 1518	. . . . . . . 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 1481	. . . . 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 1518	. . . . . 6 |- ( z = x -> ( z = z -> x = z ) )
19	10, 18	mpi 15	. . . . 5 |- ( z = x -> x = z )
20	19	alimi 1469	. . . 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 1540	. . . 4 |- ( ph -> A. z ph )
24		ax16i.1	. . . . 5 |- ( x = z -> ( ph <-> ps ) )
25	24	biimpcd 159	. . . 4 |- ( ph -> ( x = z -> ps ) )
26	23, 25	alimdh 1481	. . 3 |- ( ph -> ( A. z x = z -> A. z ps ) )
27		ax16i.2	. . . 4 |- ( ps -> A. x ps )
28	24	biimprd 158	. . . . 5 |- ( x = z -> ( ps -> ph ) )
29	19, 28	syl 14	. . . 4 |- ( z = x -> ( ps -> ph ) )
30	27, 23, 29	cbv3h 1757	. . 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 105   A.wal 1362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475

This theorem is referenced by:  ax16ALT  1873