Theorem ax12indalem 2275

Description: Lemma for ax12inda2 2277 and ax12inda 2278. (Contributed by NM, 24-Jan-2007.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
ax12indalem.1

Assertion

Ref	Expression
ax12indalem

Proof of Theorem ax12indalem

Step	Hyp	Ref	Expression
1		ax-1 6	. . . . . . . . 9
2	1	axc4i-o 2229	. . . . . . . 8
3	2	a1i 11	. . . . . . 7
4		biidd 237	. . . . . . . 8
5	4	dral1-o 2233	. . . . . . 7
6	5	imbi2d 316	. . . . . . . 8
7	6	dral2-o 2260	. . . . . . 7
8	3, 5, 7	3imtr4d 268	. . . . . 6
9	8	aecoms-o 2231	. . . . 5
10	9	a1d 25	. . . 4
11	10	a1d 25	. . 3
12	11	adantr 465	. 2
13		simplr 755	. . . . 5
14		aecom-o 2230	. . . . . . . . 9
15	14	con3i 135	. . . . . . . 8
16		aecom-o 2230	. . . . . . . . 9
17	16	con3i 135	. . . . . . . 8
18		axc9 2046	. . . . . . . . 9
19	18	imp 429	. . . . . . . 8
20	15, 17, 19	syl2an 477	. . . . . . 7
21	20	imp 429	. . . . . 6
22	21	adantlr 714	. . . . 5
23		hbnae-o 2258	. . . . . . 7
24		hba1-o 2228	. . . . . . 7
25	23, 24	hban 1931	. . . . . 6
26		ax-c5 2214	. . . . . . 7
27		ax12indalem.1	. . . . . . . 8
28	27	imp 429	. . . . . . 7
29	26, 28	sylan2 474	. . . . . 6
30	25, 29	alimdh 1638	. . . . 5
31	13, 22, 30	syl2anc 661	. . . 4
32		ax-11 1842	. . . . . 6
33		hbnae-o 2258	. . . . . . . 8
34		hbnae-o 2258	. . . . . . . 8
35	33, 34	hban 1931	. . . . . . 7
36		hbnae-o 2258	. . . . . . . . . 10
37		hbnae-o 2258	. . . . . . . . . 10
38	36, 37	hban 1931	. . . . . . . . 9
39	38, 20	nfdh 1879	. . . . . . . 8
40		19.21t 1904	. . . . . . . 8
41	39, 40	syl 16	. . . . . . 7
42	35, 41	albidh 1675	. . . . . 6
43	32, 42	syl5ib 219	. . . . 5
44	43	ad2antrr 725	. . . 4
45	31, 44	syld 44	. . 3
46	45	exp31 604	. 2
47	12, 46	pm2.61ian 790	1

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

This theorem is referenced by:  ax12inda2  2277

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