Step | Hyp | Ref
| Expression |
1 | | atoml.1 |
. . . 4
|
2 | 1 | hatomici 29218 |
. . 3
HAtoms
|
3 | | nssne2 3662 |
. . . . . . . . . . . . . . . . 17
|
4 | 3 | adantrl 752 |
. . . . . . . . . . . . . . . 16
|
5 | | atnemeq0 29236 |
. . . . . . . . . . . . . . . 16
HAtoms
HAtoms
|
6 | 4, 5 | syl5ib 234 |
. . . . . . . . . . . . . . 15
HAtoms
HAtoms
|
7 | | atelch 29203 |
. . . . . . . . . . . . . . . 16
HAtoms |
8 | | cvp 29234 |
. . . . . . . . . . . . . . . . 17
HAtoms
|
9 | | atelch 29203 |
. . . . . . . . . . . . . . . . . . 19
HAtoms |
10 | | chjcom 28365 |
. . . . . . . . . . . . . . . . . . 19
|
11 | 9, 10 | sylan2 491 |
. . . . . . . . . . . . . . . . . 18
HAtoms |
12 | 11 | breq2d 4665 |
. . . . . . . . . . . . . . . . 17
HAtoms
|
13 | 8, 12 | bitrd 268 |
. . . . . . . . . . . . . . . 16
HAtoms
|
14 | 7, 13 | sylan 488 |
. . . . . . . . . . . . . . 15
HAtoms
HAtoms
|
15 | 6, 14 | sylibd 229 |
. . . . . . . . . . . . . 14
HAtoms
HAtoms
|
16 | 15 | ancoms 469 |
. . . . . . . . . . . . 13
HAtoms
HAtoms
|
17 | 16 | adantlr 751 |
. . . . . . . . . . . 12
HAtoms HAtoms HAtoms
|
18 | 17 | imp 445 |
. . . . . . . . . . 11
HAtoms
HAtoms
HAtoms
|
19 | | chub1 28366 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
20 | 9, 7, 19 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . 24
HAtoms
HAtoms
|
21 | 20 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . 23
HAtoms
HAtoms HAtoms
|
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
HAtoms HAtoms HAtoms |
23 | | pssss 3702 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
24 | | sstr 3611 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
25 | 23, 24 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
26 | 25 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
27 | 26 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . 23
HAtoms HAtoms HAtoms |
28 | | incom 3805 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
29 | 3, 5 | syl5ib 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
HAtoms
HAtoms
|
30 | 29 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
HAtoms
HAtoms
|
31 | 30 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
HAtoms
HAtoms HAtoms
|
32 | 31 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
HAtoms HAtoms HAtoms
|
33 | 28, 32 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
HAtoms HAtoms HAtoms |
34 | 33 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . 23
HAtoms HAtoms HAtoms |
35 | | atexch 29240 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
HAtoms HAtoms
|
36 | 9, 35 | syl3an1 1359 |
. . . . . . . . . . . . . . . . . . . . . . . 24
HAtoms
HAtoms HAtoms
|
37 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
HAtoms HAtoms HAtoms
|
38 | 27, 34, 37 | mp2and 715 |
. . . . . . . . . . . . . . . . . . . . . 22
HAtoms HAtoms HAtoms |
39 | | atelch 29203 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
HAtoms |
40 | | simp1 1061 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
41 | | simp3 1063 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
42 | | chjcl 28216 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
43 | 42 | 3adant3 1081 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
44 | 40, 41, 43 | 3jca 1242 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
45 | 9, 7, 39, 44 | syl3an 1368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
HAtoms
HAtoms HAtoms
|
46 | | chlub 28368 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
47 | 45, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
HAtoms
HAtoms HAtoms
|
48 | 47 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
HAtoms HAtoms HAtoms
|
49 | 22, 38, 48 | mpbi2and 956 |
. . . . . . . . . . . . . . . . . . . . 21
HAtoms HAtoms HAtoms
|
50 | | chub1 28366 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
51 | 50 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
52 | 51, 26 | anim12i 590 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
53 | | chjcl 28216 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
54 | 53 | 3adant2 1080 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
55 | | chlub 28368 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
56 | 54, 55 | syld3an3 1371 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
57 | 56 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
58 | 52, 57 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . . . 22
|
59 | 9, 7, 39, 58 | syl3anl 1377 |
. . . . . . . . . . . . . . . . . . . . 21
HAtoms HAtoms HAtoms
|
60 | 49, 59 | eqssd 3620 |
. . . . . . . . . . . . . . . . . . . 20
HAtoms HAtoms HAtoms |
61 | 60 | anassrs 680 |
. . . . . . . . . . . . . . . . . . 19
HAtoms
HAtoms HAtoms |
62 | 61 | psseq2d 3700 |
. . . . . . . . . . . . . . . . . 18
HAtoms
HAtoms HAtoms
|
63 | 62 | ex 450 |
. . . . . . . . . . . . . . . . 17
HAtoms HAtoms HAtoms
|
64 | 63 | ibd 258 |
. . . . . . . . . . . . . . . 16
HAtoms HAtoms HAtoms |
65 | 64 | exp32 631 |
. . . . . . . . . . . . . . 15
HAtoms
HAtoms HAtoms
|
66 | 65 | 3expa 1265 |
. . . . . . . . . . . . . 14
HAtoms HAtoms HAtoms
|
67 | 66 | an32s 846 |
. . . . . . . . . . . . 13
HAtoms HAtoms HAtoms
|
68 | 67 | com34 91 |
. . . . . . . . . . . 12
HAtoms HAtoms HAtoms
|
69 | 68 | imp45 623 |
. . . . . . . . . . 11
HAtoms
HAtoms
HAtoms
|
70 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
|
71 | 70, 42 | jca 554 |
. . . . . . . . . . . . . . . 16
|
72 | 9, 7, 71 | syl2an 494 |
. . . . . . . . . . . . . . 15
HAtoms
HAtoms
|
73 | | cvnbtwn3 29147 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 1, 73 | mp3an3 1413 |
. . . . . . . . . . . . . . . . . 18
|
75 | 74 | exp4a 633 |
. . . . . . . . . . . . . . . . 17
|
76 | 75 | com23 86 |
. . . . . . . . . . . . . . . 16
|
77 | 76 | imp4a 614 |
. . . . . . . . . . . . . . 15
|
78 | 72, 77 | syl 17 |
. . . . . . . . . . . . . 14
HAtoms
HAtoms
|
79 | 78 | adantlr 751 |
. . . . . . . . . . . . 13
HAtoms HAtoms HAtoms
|
80 | 79 | imp 445 |
. . . . . . . . . . . 12
HAtoms
HAtoms
HAtoms
|
81 | 80 | adantrr 753 |
. . . . . . . . . . 11
HAtoms
HAtoms
HAtoms
|
82 | 18, 69, 81 | mp2and 715 |
. . . . . . . . . 10
HAtoms
HAtoms
HAtoms
|
83 | 82 | eleq1d 2686 |
. . . . . . . . 9
HAtoms
HAtoms
HAtoms
HAtoms
HAtoms |
84 | 83 | biimprcd 240 |
. . . . . . . 8
HAtoms HAtoms HAtoms HAtoms
HAtoms |
85 | 84 | exp4c 636 |
. . . . . . 7
HAtoms HAtoms HAtoms HAtoms
HAtoms |
86 | 85 | pm2.43b 55 |
. . . . . 6
HAtoms
HAtoms
HAtoms HAtoms |
87 | 86 | imp 445 |
. . . . 5
HAtoms HAtoms HAtoms
HAtoms |
88 | 87 | exp4d 637 |
. . . 4
HAtoms HAtoms HAtoms
HAtoms |
89 | 88 | rexlimdva 3031 |
. . 3
HAtoms
HAtoms
HAtoms HAtoms |
90 | 2, 89 | syl5 34 |
. 2
HAtoms
HAtoms
HAtoms |
91 | 90 | imp32 449 |
1
HAtoms HAtoms HAtoms |