Theorem ax12inda2ALT

Description: Alternate proof of ax12inda2 , slightly more direct and not requiring ax-c16 . (Contributed by NM, 4-May-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	ax12inda2.1	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
Assertion	ax12inda2ALT	|- ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax12inda2.1	|- ( -. A. x x = y -> ( x = y -> ( ph -> A. x ( x = y -> ph ) ) ) )
2		ax-1	|- ( A. x ph -> ( x = y -> A. x ph ) )
3	2	axc4i-o	|- ( A. x ph -> A. x ( x = y -> A. x ph ) )
4	3	a1i	|- ( A. z z = x -> ( A. x ph -> A. x ( x = y -> A. x ph ) ) )
5		biidd	|- ( A. z z = x -> ( ph <-> ph ) )
6	5	dral1-o	|- ( A. z z = x -> ( A. z ph <-> A. x ph ) )
7	6	imbi2d	|- ( A. z z = x -> ( ( x = y -> A. z ph ) <-> ( x = y -> A. x ph ) ) )
8	7	dral2-o	|- ( A. z z = x -> ( A. x ( x = y -> A. z ph ) <-> A. x ( x = y -> A. x ph ) ) )
9	4 6 8	3imtr4d	|- ( A. z z = x -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
10	9	aecoms-o	|- ( A. x x = z -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
11	10	a1d	|- ( A. x x = z -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )
12	11	a1d	|- ( A. x x = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
13		simplr	|- ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> -. A. x x = y )
14		dveeq1-o	|- ( -. A. z z = x -> ( x = y -> A. z x = y ) )
15	14	naecoms-o	|- ( -. A. x x = z -> ( x = y -> A. z x = y ) )
16	15	imp	|- ( ( -. A. x x = z /\ x = y ) -> A. z x = y )
17	16	adantlr	|- ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> A. z x = y )
18		hbnae-o	|- ( -. A. x x = y -> A. z -. A. x x = y )
19		hba1-o	|- ( A. z x = y -> A. z A. z x = y )
20	18 19	hban	|- ( ( -. A. x x = y /\ A. z x = y ) -> A. z ( -. A. x x = y /\ A. z x = y ) )
21		ax-c5	|- ( A. z x = y -> x = y )
22	1	imp	|- ( ( -. A. x x = y /\ x = y ) -> ( ph -> A. x ( x = y -> ph ) ) )
23	21 22	sylan2	|- ( ( -. A. x x = y /\ A. z x = y ) -> ( ph -> A. x ( x = y -> ph ) ) )
24	20 23	alimdh	|- ( ( -. A. x x = y /\ A. z x = y ) -> ( A. z ph -> A. z A. x ( x = y -> ph ) ) )
25	13 17 24	syl2anc	|- ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> ( A. z ph -> A. z A. x ( x = y -> ph ) ) )
26		ax-11	|- ( A. z A. x ( x = y -> ph ) -> A. x A. z ( x = y -> ph ) )
27		hbnae-o	|- ( -. A. x x = z -> A. x -. A. x x = z )
28		hbnae-o	|- ( -. A. x x = z -> A. z -. A. x x = z )
29	28 15	nf5dh	|- ( -. A. x x = z -> F/ z x = y )
30		19.21t	|- ( F/ z x = y -> ( A. z ( x = y -> ph ) <-> ( x = y -> A. z ph ) ) )
31	29 30	syl	|- ( -. A. x x = z -> ( A. z ( x = y -> ph ) <-> ( x = y -> A. z ph ) ) )
32	27 31	albidh	|- ( -. A. x x = z -> ( A. x A. z ( x = y -> ph ) <-> A. x ( x = y -> A. z ph ) ) )
33	26 32	imbitrid	|- ( -. A. x x = z -> ( A. z A. x ( x = y -> ph ) -> A. x ( x = y -> A. z ph ) ) )
34	33	ad2antrr	|- ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> ( A. z A. x ( x = y -> ph ) -> A. x ( x = y -> A. z ph ) ) )
35	25 34	syld	|- ( ( ( -. A. x x = z /\ -. A. x x = y ) /\ x = y ) -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) )
36	35	exp31	|- ( -. A. x x = z -> ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) ) )
37	12 36	pm2.61i	|- ( -. A. x x = y -> ( x = y -> ( A. z ph -> A. x ( x = y -> A. z ph ) ) ) )