Theorem axpowndlem3OLD 8997

Description: Obsolete proof of axpowndlem3 8996 as of 9-Jun-2019. (Contributed by NM, 4-Jan-2002.) (Revised by Mario Carneiro, 10-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
axpowndlem3OLD

Distinct variable group:   ,

Proof of Theorem axpowndlem3OLD

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axpowndlem2OLD 8995	. 2
2		axpowndlem1 8993	. 2
3		p0ex 4639	. . . . . . . . 9
4		eleq2 2530	. . . . . . . . . . 11
5	4	imbi2d 316	. . . . . . . . . 10
6	5	albidv 1713	. . . . . . . . 9
7	3, 6	spcev 3201	. . . . . . . 8
8		0ex 4582	. . . . . . . . . 10
9	8	snid 4057	. . . . . . . . 9
10		eleq1 2529	. . . . . . . . 9
11	9, 10	mpbiri 233	. . . . . . . 8
12	7, 11	mpg 1620	. . . . . . 7
13		neq0 3795	. . . . . . . . . . 11
14	13	con1bii 331	. . . . . . . . . 10
15	14	imbi1i 325	. . . . . . . . 9
16	15	albii 1640	. . . . . . . 8
17	16	exbii 1667	. . . . . . 7
18	12, 17	mpbir 209	. . . . . 6
19		nfnae 2058	. . . . . . 7
20		nfnae 2058	. . . . . . . 8
21		nfcvf2 2645	. . . . . . . . . . . 12
22		nfcvd 2620	. . . . . . . . . . . 12
23	21, 22	nfeld 2627	. . . . . . . . . . 11
24	19, 23	nfexd 1952	. . . . . . . . . 10
25	24	nfnd 1902	. . . . . . . . 9
26	22, 21	nfeld 2627	. . . . . . . . 9
27	25, 26	nfimd 1917	. . . . . . . 8
28		dveeq2 2042	. . . . . . . . . . . . 13
29	28	imdistani 690	. . . . . . . . . . . 12
30		nfa1 1897	. . . . . . . . . . . . . 14
31		elequ2 1823	. . . . . . . . . . . . . . 15
32	31	sps 1865	. . . . . . . . . . . . . 14
33	30, 32	exbid 1886	. . . . . . . . . . . . 13
34	33	adantl 466	. . . . . . . . . . . 12
35	29, 34	syl 16	. . . . . . . . . . 11
36	35	notbid 294	. . . . . . . . . 10
37		elequ1 1821	. . . . . . . . . . 11
38	37	adantl 466	. . . . . . . . . 10
39	36, 38	imbi12d 320	. . . . . . . . 9
40	39	ex 434	. . . . . . . 8
41	20, 27, 40	cbvald 2025	. . . . . . 7
42	19, 41	exbid 1886	. . . . . 6
43	18, 42	mpbii 211	. . . . 5
44		nfae 2056	. . . . . 6
45		nfae 2056	. . . . . . 7
46		axc11 2054	. . . . . . . . . . . 12
47	46	aecoms 2052	. . . . . . . . . . 11
48		alnex 1614	. . . . . . . . . . 11
49		alnex 1614	. . . . . . . . . . 11
50	47, 48, 49	3imtr3g 269	. . . . . . . . . 10
51		nd3 8985	. . . . . . . . . . 11
52	51	pm2.21d 106	. . . . . . . . . 10
53	50, 52	jad 162	. . . . . . . . 9
54	53	spsd 1867	. . . . . . . 8
55	54	imim1d 75	. . . . . . 7
56	45, 55	alimd 1876	. . . . . 6
57	44, 56	eximd 1882	. . . . 5
58	43, 57	syl5 32	. . . 4
59	58	a1dd 46	. . 3
60	59, 2	pm2.61d2 160	. 2
61	1, 2, 60	pm2.61ii 165	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  =wceq 1395  E.wex 1612  e.wcel 1818  c0 3784  {csn 4029

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-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-reg 8039

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-pw 4014  df-sn 4030  df-pr 4032