Step | Hyp | Ref
| Expression |
1 | | atcvat3.1 |
. . . . . . . . 9
ā¢ š“ ā
Cā |
2 | 1 | hatomici 31343 |
. . . . . . . 8
ā¢ (š“ ā 0ā ā
āš„ ā HAtoms
š„ ā š“) |
3 | | atelch 31328 |
. . . . . . . . . . . . . . 15
ā¢ (š¶ ā HAtoms ā š¶ ā
Cā ) |
4 | | atelch 31328 |
. . . . . . . . . . . . . . 15
ā¢ (š„ ā HAtoms ā š„ ā
Cā ) |
5 | | chub1 30491 |
. . . . . . . . . . . . . . 15
ā¢ ((š¶ ā
Cā ā§ š„ ā Cā )
ā š¶ ā (š¶ āØā š„)) |
6 | 3, 4, 5 | syl2an 597 |
. . . . . . . . . . . . . 14
ā¢ ((š¶ ā HAtoms ā§ š„ ā HAtoms) ā š¶ ā (š¶ āØā š„)) |
7 | | sseq1 3970 |
. . . . . . . . . . . . . 14
ā¢ (šµ = š¶ ā (šµ ā (š¶ āØā š„) ā š¶ ā (š¶ āØā š„))) |
8 | 6, 7 | syl5ibr 246 |
. . . . . . . . . . . . 13
ā¢ (šµ = š¶ ā ((š¶ ā HAtoms ā§ š„ ā HAtoms) ā šµ ā (š¶ āØā š„))) |
9 | 8 | expd 417 |
. . . . . . . . . . . 12
ā¢ (šµ = š¶ ā (š¶ ā HAtoms ā (š„ ā HAtoms ā šµ ā (š¶ āØā š„)))) |
10 | 9 | impcom 409 |
. . . . . . . . . . 11
ā¢ ((š¶ ā HAtoms ā§ šµ = š¶) ā (š„ ā HAtoms ā šµ ā (š¶ āØā š„))) |
11 | 10 | anim2d 613 |
. . . . . . . . . 10
ā¢ ((š¶ ā HAtoms ā§ šµ = š¶) ā ((š„ ā š“ ā§ š„ ā HAtoms) ā (š„ ā š“ ā§ šµ ā (š¶ āØā š„)))) |
12 | 11 | expcomd 418 |
. . . . . . . . 9
ā¢ ((š¶ ā HAtoms ā§ šµ = š¶) ā (š„ ā HAtoms ā (š„ ā š“ ā (š„ ā š“ ā§ šµ ā (š¶ āØā š„))))) |
13 | 12 | reximdvai 3159 |
. . . . . . . 8
ā¢ ((š¶ ā HAtoms ā§ šµ = š¶) ā (āš„ ā HAtoms š„ ā š“ ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„)))) |
14 | 2, 13 | syl5 34 |
. . . . . . 7
ā¢ ((š¶ ā HAtoms ā§ šµ = š¶) ā (š“ ā 0ā ā
āš„ ā HAtoms
(š„ ā š“ ā§ šµ ā (š¶ āØā š„)))) |
15 | 14 | ex 414 |
. . . . . 6
ā¢ (š¶ ā HAtoms ā (šµ = š¶ ā (š“ ā 0ā ā
āš„ ā HAtoms
(š„ ā š“ ā§ šµ ā (š¶ āØā š„))))) |
16 | 15 | a1i 11 |
. . . . 5
ā¢ (šµ ā (š“ āØā š¶) ā (š¶ ā HAtoms ā (šµ = š¶ ā (š“ ā 0ā ā
āš„ ā HAtoms
(š„ ā š“ ā§ šµ ā (š¶ āØā š„)))))) |
17 | 16 | com4l 92 |
. . . 4
ā¢ (š¶ ā HAtoms ā (šµ = š¶ ā (š“ ā 0ā ā (šµ ā (š“ āØā š¶) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„)))))) |
18 | 17 | imp4a 424 |
. . 3
ā¢ (š¶ ā HAtoms ā (šµ = š¶ ā ((š“ ā 0ā ā§ šµ ā (š“ āØā š¶)) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))))) |
19 | 18 | adantl 483 |
. 2
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (šµ = š¶ ā ((š“ ā 0ā ā§ šµ ā (š“ āØā š¶)) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))))) |
20 | | atelch 31328 |
. . . . . . . 8
ā¢ (šµ ā HAtoms ā šµ ā
Cā ) |
21 | | chlejb2 30497 |
. . . . . . . . . . . . . . 15
ā¢ ((š¶ ā
Cā ā§ š“ ā Cā )
ā (š¶ ā š“ ā (š“ āØā š¶) = š“)) |
22 | 1, 21 | mpan2 690 |
. . . . . . . . . . . . . 14
ā¢ (š¶ ā
Cā ā (š¶ ā š“ ā (š“ āØā š¶) = š“)) |
23 | 22 | biimpa 478 |
. . . . . . . . . . . . 13
ā¢ ((š¶ ā
Cā ā§ š¶ ā š“) ā (š“ āØā š¶) = š“) |
24 | 23 | sseq2d 3977 |
. . . . . . . . . . . 12
ā¢ ((š¶ ā
Cā ā§ š¶ ā š“) ā (šµ ā (š“ āØā š¶) ā šµ ā š“)) |
25 | 24 | biimpa 478 |
. . . . . . . . . . 11
ā¢ (((š¶ ā
Cā ā§ š¶ ā š“) ā§ šµ ā (š“ āØā š¶)) ā šµ ā š“) |
26 | 25 | expl 459 |
. . . . . . . . . 10
ā¢ (š¶ ā
Cā ā ((š¶ ā š“ ā§ šµ ā (š“ āØā š¶)) ā šµ ā š“)) |
27 | 26 | adantl 483 |
. . . . . . . . 9
ā¢ ((šµ ā
Cā ā§ š¶ ā Cā )
ā ((š¶ ā š“ ā§ šµ ā (š“ āØā š¶)) ā šµ ā š“)) |
28 | | chub2 30492 |
. . . . . . . . 9
ā¢ ((šµ ā
Cā ā§ š¶ ā Cā )
ā šµ ā (š¶ āØā šµ)) |
29 | 27, 28 | jctird 528 |
. . . . . . . 8
ā¢ ((šµ ā
Cā ā§ š¶ ā Cā )
ā ((š¶ ā š“ ā§ šµ ā (š“ āØā š¶)) ā (šµ ā š“ ā§ šµ ā (š¶ āØā šµ)))) |
30 | 20, 3, 29 | syl2an 597 |
. . . . . . 7
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā ((š¶ ā š“ ā§ šµ ā (š“ āØā š¶)) ā (šµ ā š“ ā§ šµ ā (š¶ āØā šµ)))) |
31 | | simpl 484 |
. . . . . . 7
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā šµ ā HAtoms) |
32 | 30, 31 | jctild 527 |
. . . . . 6
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā ((š¶ ā š“ ā§ šµ ā (š“ āØā š¶)) ā (šµ ā HAtoms ā§ (šµ ā š“ ā§ šµ ā (š¶ āØā šµ))))) |
33 | 32 | impl 457 |
. . . . 5
ā¢ ((((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ š¶ ā š“) ā§ šµ ā (š“ āØā š¶)) ā (šµ ā HAtoms ā§ (šµ ā š“ ā§ šµ ā (š¶ āØā šµ)))) |
34 | | sseq1 3970 |
. . . . . . 7
ā¢ (š„ = šµ ā (š„ ā š“ ā šµ ā š“)) |
35 | | oveq2 7366 |
. . . . . . . 8
ā¢ (š„ = šµ ā (š¶ āØā š„) = (š¶ āØā šµ)) |
36 | 35 | sseq2d 3977 |
. . . . . . 7
ā¢ (š„ = šµ ā (šµ ā (š¶ āØā š„) ā šµ ā (š¶ āØā šµ))) |
37 | 34, 36 | anbi12d 632 |
. . . . . 6
ā¢ (š„ = šµ ā ((š„ ā š“ ā§ šµ ā (š¶ āØā š„)) ā (šµ ā š“ ā§ šµ ā (š¶ āØā šµ)))) |
38 | 37 | rspcev 3580 |
. . . . 5
ā¢ ((šµ ā HAtoms ā§ (šµ ā š“ ā§ šµ ā (š¶ āØā šµ))) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))) |
39 | 33, 38 | syl 17 |
. . . 4
ā¢ ((((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ š¶ ā š“) ā§ šµ ā (š“ āØā š¶)) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))) |
40 | 39 | adantrl 715 |
. . 3
ā¢ ((((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ š¶ ā š“) ā§ (š“ ā 0ā ā§ šµ ā (š“ āØā š¶))) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))) |
41 | 40 | exp31 421 |
. 2
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (š¶ ā š“ ā ((š“ ā 0ā ā§ šµ ā (š“ āØā š¶)) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))))) |
42 | | simpr 486 |
. . 3
ā¢ ((š“ ā 0ā ā§
šµ ā (š“ āØā š¶)) ā šµ ā (š“ āØā š¶)) |
43 | | ioran 983 |
. . . 4
ā¢ (Ā¬
(šµ = š¶ āØ š¶ ā š“) ā (Ā¬ šµ = š¶ ā§ Ā¬ š¶ ā š“)) |
44 | 1 | atcvat3i 31380 |
. . . . . . 7
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶)) ā (š“ ā© (šµ āØā š¶)) ā HAtoms)) |
45 | 3 | ad2antlr 726 |
. . . . . . . . . . 11
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā š¶ ā Cā
) |
46 | 44 | imp 408 |
. . . . . . . . . . 11
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā (š“ ā© (šµ āØā š¶)) ā HAtoms) |
47 | | simpll 766 |
. . . . . . . . . . 11
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā šµ ā HAtoms) |
48 | 45, 46, 47 | 3jca 1129 |
. . . . . . . . . 10
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā (š¶ ā Cā
ā§ (š“ ā© (šµ āØā š¶)) ā HAtoms ā§ šµ ā
HAtoms)) |
49 | | inss2 4190 |
. . . . . . . . . . . . 13
ā¢ (š“ ā© (šµ āØā š¶)) ā (šµ āØā š¶) |
50 | | chjcom 30490 |
. . . . . . . . . . . . . 14
ā¢ ((šµ ā
Cā ā§ š¶ ā Cā )
ā (šµ
āØā š¶) =
(š¶ āØā
šµ)) |
51 | 20, 3, 50 | syl2an 597 |
. . . . . . . . . . . . 13
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (šµ āØā š¶) = (š¶ āØā šµ)) |
52 | 49, 51 | sseqtrid 3997 |
. . . . . . . . . . . 12
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (š“ ā© (šµ āØā š¶)) ā (š¶ āØā šµ)) |
53 | 52 | adantr 482 |
. . . . . . . . . . 11
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā (š“ ā© (šµ āØā š¶)) ā (š¶ āØā šµ)) |
54 | | atnssm0 31360 |
. . . . . . . . . . . . . . . . 17
ā¢ ((š“ ā
Cā ā§ š¶ ā HAtoms) ā (Ā¬ š¶ ā š“ ā (š“ ā© š¶) = 0ā)) |
55 | 1, 54 | mpan 689 |
. . . . . . . . . . . . . . . 16
ā¢ (š¶ ā HAtoms ā (Ā¬
š¶ ā š“ ā (š“ ā© š¶) = 0ā)) |
56 | 55 | adantl 483 |
. . . . . . . . . . . . . . 15
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (Ā¬
š¶ ā š“ ā (š“ ā© š¶) = 0ā)) |
57 | | inss1 4189 |
. . . . . . . . . . . . . . . . . . 19
ā¢ (š“ ā© (šµ āØā š¶)) ā š“ |
58 | | sslin 4195 |
. . . . . . . . . . . . . . . . . . 19
ā¢ ((š“ ā© (šµ āØā š¶)) ā š“ ā (š¶ ā© (š“ ā© (šµ āØā š¶))) ā (š¶ ā© š“)) |
59 | 57, 58 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
ā¢ (š¶ ā© (š“ ā© (šµ āØā š¶))) ā (š¶ ā© š“) |
60 | | incom 4162 |
. . . . . . . . . . . . . . . . . 18
ā¢ (š¶ ā© š“) = (š“ ā© š¶) |
61 | 59, 60 | sseqtri 3981 |
. . . . . . . . . . . . . . . . 17
ā¢ (š¶ ā© (š“ ā© (šµ āØā š¶))) ā (š“ ā© š¶) |
62 | | sseq2 3971 |
. . . . . . . . . . . . . . . . 17
ā¢ ((š“ ā© š¶) = 0ā ā ((š¶ ā© (š“ ā© (šµ āØā š¶))) ā (š“ ā© š¶) ā (š¶ ā© (š“ ā© (šµ āØā š¶))) ā
0ā)) |
63 | 61, 62 | mpbii 232 |
. . . . . . . . . . . . . . . 16
ā¢ ((š“ ā© š¶) = 0ā ā (š¶ ā© (š“ ā© (šµ āØā š¶))) ā
0ā) |
64 | | simpr 486 |
. . . . . . . . . . . . . . . . . . 19
ā¢ ((šµ ā
Cā ā§ š¶ ā Cā )
ā š¶ ā
Cā ) |
65 | | chjcl 30341 |
. . . . . . . . . . . . . . . . . . . 20
ā¢ ((šµ ā
Cā ā§ š¶ ā Cā )
ā (šµ
āØā š¶)
ā Cā ) |
66 | | chincl 30483 |
. . . . . . . . . . . . . . . . . . . 20
ā¢ ((š“ ā
Cā ā§ (šµ āØā š¶) ā Cā )
ā (š“ ā© (šµ āØā š¶)) ā
Cā ) |
67 | 1, 65, 66 | sylancr 588 |
. . . . . . . . . . . . . . . . . . 19
ā¢ ((šµ ā
Cā ā§ š¶ ā Cā )
ā (š“ ā© (šµ āØā š¶)) ā
Cā ) |
68 | | chincl 30483 |
. . . . . . . . . . . . . . . . . . 19
ā¢ ((š¶ ā
Cā ā§ (š“ ā© (šµ āØā š¶)) ā Cā
) ā (š¶ ā© (š“ ā© (šµ āØā š¶))) ā Cā
) |
69 | 64, 67, 68 | syl2anc 585 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((šµ ā
Cā ā§ š¶ ā Cā )
ā (š¶ ā© (š“ ā© (šµ āØā š¶))) ā Cā
) |
70 | 20, 3, 69 | syl2an 597 |
. . . . . . . . . . . . . . . . 17
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (š¶ ā© (š“ ā© (šµ āØā š¶))) ā Cā
) |
71 | | chle0 30427 |
. . . . . . . . . . . . . . . . 17
ā¢ ((š¶ ā© (š“ ā© (šµ āØā š¶))) ā Cā
ā ((š¶ ā© (š“ ā© (šµ āØā š¶))) ā 0ā ā
(š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā ((š¶ ā© (š“ ā© (šµ āØā š¶))) ā 0ā ā
(š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā)) |
73 | 63, 72 | imbitrid 243 |
. . . . . . . . . . . . . . 15
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā ((š“ ā© š¶) = 0ā ā (š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā)) |
74 | 56, 73 | sylbid 239 |
. . . . . . . . . . . . . 14
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (Ā¬
š¶ ā š“ ā (š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā)) |
75 | 74 | imp 408 |
. . . . . . . . . . . . 13
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ Ā¬
š¶ ā š“) ā (š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā) |
76 | 75 | adantrl 715 |
. . . . . . . . . . . 12
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ (Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“)) ā (š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā) |
77 | 76 | adantrr 716 |
. . . . . . . . . . 11
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā (š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā) |
78 | 53, 77 | jca 513 |
. . . . . . . . . 10
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā ((š“ ā© (šµ āØā š¶)) ā (š¶ āØā šµ) ā§ (š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā)) |
79 | | atexch 31365 |
. . . . . . . . . 10
ā¢ ((š¶ ā
Cā ā§ (š“ ā© (šµ āØā š¶)) ā HAtoms ā§ šµ ā HAtoms) ā (((š“ ā© (šµ āØā š¶)) ā (š¶ āØā šµ) ā§ (š¶ ā© (š“ ā© (šµ āØā š¶))) = 0ā) ā šµ ā (š¶ āØā (š“ ā© (šµ āØā š¶))))) |
80 | 48, 78, 79 | sylc 65 |
. . . . . . . . 9
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā šµ ā (š¶ āØā (š“ ā© (šµ āØā š¶)))) |
81 | 80, 57 | jctil 521 |
. . . . . . . 8
ā¢ (((šµ ā HAtoms ā§ š¶ ā HAtoms) ā§ ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶))) ā ((š“ ā© (šµ āØā š¶)) ā š“ ā§ šµ ā (š¶ āØā (š“ ā© (šµ āØā š¶))))) |
82 | 81 | ex 414 |
. . . . . . 7
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶)) ā ((š“ ā© (šµ āØā š¶)) ā š“ ā§ šµ ā (š¶ āØā (š“ ā© (šµ āØā š¶)))))) |
83 | 44, 82 | jcad 514 |
. . . . . 6
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶)) ā ((š“ ā© (šµ āØā š¶)) ā HAtoms ā§ ((š“ ā© (šµ āØā š¶)) ā š“ ā§ šµ ā (š¶ āØā (š“ ā© (šµ āØā š¶))))))) |
84 | | sseq1 3970 |
. . . . . . . 8
ā¢ (š„ = (š“ ā© (šµ āØā š¶)) ā (š„ ā š“ ā (š“ ā© (šµ āØā š¶)) ā š“)) |
85 | | oveq2 7366 |
. . . . . . . . 9
ā¢ (š„ = (š“ ā© (šµ āØā š¶)) ā (š¶ āØā š„) = (š¶ āØā (š“ ā© (šµ āØā š¶)))) |
86 | 85 | sseq2d 3977 |
. . . . . . . 8
ā¢ (š„ = (š“ ā© (šµ āØā š¶)) ā (šµ ā (š¶ āØā š„) ā šµ ā (š¶ āØā (š“ ā© (šµ āØā š¶))))) |
87 | 84, 86 | anbi12d 632 |
. . . . . . 7
ā¢ (š„ = (š“ ā© (šµ āØā š¶)) ā ((š„ ā š“ ā§ šµ ā (š¶ āØā š„)) ā ((š“ ā© (šµ āØā š¶)) ā š“ ā§ šµ ā (š¶ āØā (š“ ā© (šµ āØā š¶)))))) |
88 | 87 | rspcev 3580 |
. . . . . 6
ā¢ (((š“ ā© (šµ āØā š¶)) ā HAtoms ā§ ((š“ ā© (šµ āØā š¶)) ā š“ ā§ šµ ā (š¶ āØā (š“ ā© (šµ āØā š¶))))) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))) |
89 | 83, 88 | syl6 35 |
. . . . 5
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā§ šµ ā (š“ āØā š¶)) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„)))) |
90 | 89 | expd 417 |
. . . 4
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā ((Ā¬
šµ = š¶ ā§ Ā¬ š¶ ā š“) ā (šµ ā (š“ āØā š¶) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))))) |
91 | 43, 90 | biimtrid 241 |
. . 3
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (Ā¬
(šµ = š¶ āØ š¶ ā š“) ā (šµ ā (š“ āØā š¶) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))))) |
92 | 42, 91 | syl7 74 |
. 2
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā (Ā¬
(šµ = š¶ āØ š¶ ā š“) ā ((š“ ā 0ā ā§ šµ ā (š“ āØā š¶)) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„))))) |
93 | 19, 41, 92 | ecase3d 1033 |
1
ā¢ ((šµ ā HAtoms ā§ š¶ ā HAtoms) ā ((š“ ā 0ā ā§
šµ ā (š“ āØā š¶)) ā āš„ ā HAtoms (š„ ā š“ ā§ šµ ā (š¶ āØā š„)))) |