MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axpowndlem3OLD Unicode version

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.
StepHypRef Expression
1 axpowndlem2OLD 8995 . 2
2 axpowndlem1 8993 . 2
3 p0ex 4639 . . . . . . . . 9
4 eleq2 2530 . . . . . . . . . . 11
54imbi2d 316 . . . . . . . . . 10
65albidv 1713 . . . . . . . . 9
73, 6spcev 3201 . . . . . . . 8
8 0ex 4582 . . . . . . . . . 10
98snid 4057 . . . . . . . . 9
10 eleq1 2529 . . . . . . . . 9
119, 10mpbiri 233 . . . . . . . 8
127, 11mpg 1620 . . . . . . 7
13 neq0 3795 . . . . . . . . . . 11
1413con1bii 331 . . . . . . . . . 10
1514imbi1i 325 . . . . . . . . 9
1615albii 1640 . . . . . . . 8
1716exbii 1667 . . . . . . 7
1812, 17mpbir 209 . . . . . 6
19 nfnae 2058 . . . . . . 7
20 nfnae 2058 . . . . . . . 8
21 nfcvf2 2645 . . . . . . . . . . . 12
22 nfcvd 2620 . . . . . . . . . . . 12
2321, 22nfeld 2627 . . . . . . . . . . 11
2419, 23nfexd 1952 . . . . . . . . . 10
2524nfnd 1902 . . . . . . . . 9
2622, 21nfeld 2627 . . . . . . . . 9
2725, 26nfimd 1917 . . . . . . . 8
28 dveeq2 2042 . . . . . . . . . . . . 13
2928imdistani 690 . . . . . . . . . . . 12
30 nfa1 1897 . . . . . . . . . . . . . 14
31 elequ2 1823 . . . . . . . . . . . . . . 15
3231sps 1865 . . . . . . . . . . . . . 14
3330, 32exbid 1886 . . . . . . . . . . . . 13
3433adantl 466 . . . . . . . . . . . 12
3529, 34syl 16 . . . . . . . . . . 11
3635notbid 294 . . . . . . . . . 10
37 elequ1 1821 . . . . . . . . . . 11
3837adantl 466 . . . . . . . . . 10
3936, 38imbi12d 320 . . . . . . . . 9
4039ex 434 . . . . . . . 8
4120, 27, 40cbvald 2025 . . . . . . 7
4219, 41exbid 1886 . . . . . 6
4318, 42mpbii 211 . . . . 5
44 nfae 2056 . . . . . 6
45 nfae 2056 . . . . . . 7
46 axc11 2054 . . . . . . . . . . . 12
4746aecoms 2052 . . . . . . . . . . 11
48 alnex 1614 . . . . . . . . . . 11
49 alnex 1614 . . . . . . . . . . 11
5047, 48, 493imtr3g 269 . . . . . . . . . 10
51 nd3 8985 . . . . . . . . . . 11
5251pm2.21d 106 . . . . . . . . . 10
5350, 52jad 162 . . . . . . . . 9
5453spsd 1867 . . . . . . . 8
5554imim1d 75 . . . . . . 7
5645, 55alimd 1876 . . . . . 6
5744, 56eximd 1882 . . . . 5
5843, 57syl5 32 . . . 4
5958a1dd 46 . . 3
6059, 2pm2.61d2 160 . 2
611, 2, 60pm2.61ii 165 1
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator