Theorem ax16i 1779

Description: Inference with ax-16 1735 as its conclusion, that doesn't require ax-10 1436, ax-11 1437, or ax-12 1442 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 1459	. . . 4 |- ( x = y -> A. z x = y )
2		ax-17 1459	. . . 4 |- ( z = y -> A. x z = y )
3		ax-8 1435	. . . 4 |- ( x = z -> ( x = y -> z = y ) )
4	1, 2, 3	cbv3h 1671	. . 3 |- ( A. x x = y -> A. z z = y )
5		ax-8 1435	. . . . . 6 |- ( z = x -> ( z = y -> x = y ) )
6	5	spimv 1732	. . . . 5 |- ( A. z z = y -> x = y )
7		equid 1629	. . . . . . . 8 |- x = x
8		ax-8 1435	. . . . . . . 8 |- ( x = y -> ( x = x -> y = x ) )
9	7, 8	mpi 15	. . . . . . 7 |- ( x = y -> y = x )
10		equid 1629	. . . . . . . . 9 |- z = z
11		ax-8 1435	. . . . . . . . 9 |- ( z = y -> ( z = z -> y = z ) )
12	10, 11	mpi 15	. . . . . . . 8 |- ( z = y -> y = z )
13		ax-8 1435	. . . . . . . 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 1396	. . . . 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 1435	. . . . . 6 |- ( z = x -> ( z = z -> x = z ) )
19	10, 18	mpi 15	. . . . 5 |- ( z = x -> x = z )
20	19	alimi 1384	. . . 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 1459	. . . 4 |- ( ph -> A. z ph )
24		ax16i.1	. . . . 5 |- ( x = z -> ( ph <-> ps ) )
25	24	biimpcd 157	. . . 4 |- ( ph -> ( x = z -> ps ) )
26	23, 25	alimdh 1396	. . 3 |- ( ph -> ( A. z x = z -> A. z ps ) )
27		ax16i.2	. . . 4 |- ( ps -> A. x ps )
28	24	biimprd 156	. . . . 5 |- ( x = z -> ( ps -> ph ) )
29	19, 28	syl 14	. . . 4 |- ( z = x -> ( ps -> ph ) )
30	27, 23, 29	cbv3h 1671	. . 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 103   A.wal 1282

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467

This theorem depends on definitions:  df-bi 115  df-nf 1390

This theorem is referenced by:  ax16ALT  1780