Theorem ax12inda2ALT 2276

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

Hypothesis

Ref	Expression
ax12inda2.1

Assertion

Ref	Expression
ax12inda2ALT

Distinct variable group:   ,

Proof of Theorem ax12inda2ALT

Step	Hyp	Ref	Expression
1		ax-1 6	. . . . . . . 8
2	1	axc4i-o 2229	. . . . . . 7
3	2	a1i 11	. . . . . 6
4		biidd 237	. . . . . . 7
5	4	dral1-o 2233	. . . . . 6
6	5	imbi2d 316	. . . . . . 7
7	6	dral2-o 2260	. . . . . 6
8	3, 5, 7	3imtr4d 268	. . . . 5
9	8	aecoms-o 2231	. . . 4
10	9	a1d 25	. . 3
11	10	a1d 25	. 2
12		simplr 755	. . . . 5
13		dveeq1-o 2265	. . . . . . . 8
14	13	naecoms-o 2257	. . . . . . 7
15	14	imp 429	. . . . . 6
16	15	adantlr 714	. . . . 5
17		hbnae-o 2258	. . . . . . 7
18		hba1-o 2228	. . . . . . 7
19	17, 18	hban 1931	. . . . . 6
20		ax-c5 2214	. . . . . . 7
21		ax12inda2.1	. . . . . . . 8
22	21	imp 429	. . . . . . 7
23	20, 22	sylan2 474	. . . . . 6
24	19, 23	alimdh 1638	. . . . 5
25	12, 16, 24	syl2anc 661	. . . 4
26		ax-11 1842	. . . . . 6
27		hbnae-o 2258	. . . . . . 7
28		hbnae-o 2258	. . . . . . . . 9
29	28, 14	nfdh 1879	. . . . . . . 8
30		19.21t 1904	. . . . . . . 8
31	29, 30	syl 16	. . . . . . 7
32	27, 31	albidh 1675	. . . . . 6
33	26, 32	syl5ib 219	. . . . 5
34	33	ad2antrr 725	. . . 4
35	25, 34	syld 44	. . 3
36	35	exp31 604	. 2
37	11, 36	pm2.61i 164	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  F/wnf 1616

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-c5 2214  ax-c4 2215  ax-c7 2216  ax-c11 2218  ax-c9 2221

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-nf 1617