Theorem axpowndlem2OLD 8995

Description: Obsolete version of axpowndlem2 8994 as of 9-Jun-2019. (Contributed by NM, 4-Jan-2002.) (Proof shortened by Mario Carneiro, 6-Dec-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
axpowndlem2OLD

Distinct variable group:   ,

Proof of Theorem axpowndlem2OLD

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		zfpow 4631	. . . . . 6
2		19.8a 1857	. . . . . . . . . . 11
3		sp 1859	. . . . . . . . . . 11
4	2, 3	imim12i 57	. . . . . . . . . 10
5	4	alimi 1633	. . . . . . . . 9
6	5	imim1i 58	. . . . . . . 8
7	6	alimi 1633	. . . . . . 7
8	7	eximi 1656	. . . . . 6
9	1, 8	mp1i 12	. . . . 5
10	9	ax-gen 1618	. . . 4
11		nfnae 2058	. . . . . 6
12		nfnae 2058	. . . . . 6
13	11, 12	nfan 1928	. . . . 5
14		nfcvd 2620	. . . . . . . 8
15		nfcvf 2644	. . . . . . . . 9
16	15	adantr 465	. . . . . . . 8
17	14, 16	nfeqd 2626	. . . . . . 7
18	17	nfnd 1902	. . . . . 6
19		nfv 1707	. . . . . . 7
20		nfnae 2058	. . . . . . . . 9
21		nfnae 2058	. . . . . . . . 9
22	20, 21	nfan 1928	. . . . . . . 8
23		nfnae 2058	. . . . . . . . . . . . 13
24		nfnae 2058	. . . . . . . . . . . . 13
25	23, 24	nfan 1928	. . . . . . . . . . . 12
26	14, 16	nfeld 2627	. . . . . . . . . . . 12
27	25, 26	nfexd 1952	. . . . . . . . . . 11
28		nfcvf 2644	. . . . . . . . . . . . . 14
29	28	adantl 466	. . . . . . . . . . . . 13
30	14, 29	nfeld 2627	. . . . . . . . . . . 12
31	22, 30	nfald 1951	. . . . . . . . . . 11
32	27, 31	nfimd 1917	. . . . . . . . . 10
33	19, 32	nfald 1951	. . . . . . . . 9
34	16, 14	nfeld 2627	. . . . . . . . 9
35	33, 34	nfimd 1917	. . . . . . . 8
36	22, 35	nfald 1951	. . . . . . 7
37	19, 36	nfexd 1952	. . . . . 6
38	18, 37	nfimd 1917	. . . . 5
39		equequ1 1798	. . . . . . . . 9
40	39	notbid 294	. . . . . . . 8
41	40	adantl 466	. . . . . . 7
42		nfcvd 2620	. . . . . . . . . . . . 13
43		nfcvf2 2645	. . . . . . . . . . . . . 14
44	43	adantr 465	. . . . . . . . . . . . 13
45	42, 44	nfeqd 2626	. . . . . . . . . . . 12
46	22, 45	nfan1 1927	. . . . . . . . . . 11
47		nfcvd 2620	. . . . . . . . . . . . . . . . . . 19
48		nfcvf2 2645	. . . . . . . . . . . . . . . . . . . 20
49	48	adantl 466	. . . . . . . . . . . . . . . . . . 19
50	47, 49	nfeqd 2626	. . . . . . . . . . . . . . . . . 18
51	25, 50	nfan1 1927	. . . . . . . . . . . . . . . . 17
52		elequ1 1821	. . . . . . . . . . . . . . . . . 18
53	52	adantl 466	. . . . . . . . . . . . . . . . 17
54	51, 53	exbid 1886	. . . . . . . . . . . . . . . 16
55		elequ1 1821	. . . . . . . . . . . . . . . . . 18
56	55	adantl 466	. . . . . . . . . . . . . . . . 17
57	46, 56	albid 1885	. . . . . . . . . . . . . . . 16
58	54, 57	imbi12d 320	. . . . . . . . . . . . . . 15
59	58	ex 434	. . . . . . . . . . . . . 14
60	13, 32, 59	cbvald 2025	. . . . . . . . . . . . 13
61	60	adantr 465	. . . . . . . . . . . 12
62		elequ2 1823	. . . . . . . . . . . . 13
63	62	adantl 466	. . . . . . . . . . . 12
64	61, 63	imbi12d 320	. . . . . . . . . . 11
65	46, 64	albid 1885	. . . . . . . . . 10
66	65	ex 434	. . . . . . . . 9
67	13, 36, 66	cbvexd 2026	. . . . . . . 8
68	67	adantr 465	. . . . . . 7
69	41, 68	imbi12d 320	. . . . . 6
70	69	ex 434	. . . . 5
71	13, 38, 70	cbvald 2025	. . . 4
72	10, 71	mpbii 211	. . 3
73	72	19.21bi 1869	. 2
74	73	ex 434	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E.wex 1612  F/_wnfc 2605

This theorem is referenced by:  axpowndlem3OLD  8997

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-pow 4630

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607