Theorem axc16i 2322

Description: Inference with axc16 2135 as its conclusion. (Contributed by NM, 20-May-2008.) (Proof modification is discouraged.)

Hypotheses

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

Assertion

Ref	Expression
axc16i	|- ( 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 axc16i

Step	Hyp	Ref	Expression
1		nfv 1843	. . 3 |- F/ z x = y
2		nfv 1843	. . 3 |- F/ x z = y
3		ax7 1943	. . 3 |- ( x = z -> ( x = y -> z = y ) )
4	1, 2, 3	cbv3 2265	. 2 |- ( A. x x = y -> A. z z = y )
5		ax7 1943	. . . . 5 |- ( z = x -> ( z = y -> x = y ) )
6	5	spimv 2257	. . . 4 |- ( A. z z = y -> x = y )
7		equcomi 1944	. . . . . 6 |- ( x = y -> y = x )
8		equcomi 1944	. . . . . . 7 |- ( z = y -> y = z )
9		ax7 1943	. . . . . . 7 |- ( y = z -> ( y = x -> z = x ) )
10	8, 9	syl 17	. . . . . 6 |- ( z = y -> ( y = x -> z = x ) )
11	7, 10	syl5com 31	. . . . 5 |- ( x = y -> ( z = y -> z = x ) )
12	11	alimdv 1845	. . . 4 |- ( x = y -> ( A. z z = y -> A. z z = x ) )
13	6, 12	mpcom 38	. . 3 |- ( A. z z = y -> A. z z = x )
14		equcomi 1944	. . . 4 |- ( z = x -> x = z )
15	14	alimi 1739	. . 3 |- ( A. z z = x -> A. z x = z )
16	13, 15	syl 17	. 2 |- ( A. z z = y -> A. z x = z )
17		axc16i.1	. . . . 5 |- ( x = z -> ( ph <-> ps ) )
18	17	biimpcd 239	. . . 4 |- ( ph -> ( x = z -> ps ) )
19	18	alimdv 1845	. . 3 |- ( ph -> ( A. z x = z -> A. z ps ) )
20		axc16i.2	. . . . 5 |- ( ps -> A. x ps )
21	20	nf5i 2024	. . . 4 |- F/ x ps
22		nfv 1843	. . . 4 |- F/ z ph
23	17	biimprd 238	. . . . 5 |- ( x = z -> ( ps -> ph ) )
24	14, 23	syl 17	. . . 4 |- ( z = x -> ( ps -> ph ) )
25	21, 22, 24	cbv3 2265	. . 3 |- ( A. z ps -> A. x ph )
26	19, 25	syl6com 37	. 2 |- ( A. z x = z -> ( ph -> A. x ph ) )
27	4, 16, 26	3syl 18	1 |- ( A. x x = y -> ( ph -> A. x ph ) )

Syntax hints:   -> wi 4   <-> wb 196   A.wal 1481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-nf 1710

This theorem is referenced by:  axc16ALT  2366