Step | Hyp | Ref
| Expression |
1 | | elxp 5700 |
. . . . . . . 8
ā¢ (š” ā (š“ Ć šµ) ā āšāš(š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ))) |
2 | | elxp 5700 |
. . . . . . . 8
ā¢ (š¢ ā (š“ Ć šµ) ā āšāš(š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ))) |
3 | | elxp 5700 |
. . . . . . . 8
ā¢ (š£ ā (š“ Ć šµ) ā āšāš(š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ))) |
4 | | 3an6 1444 |
. . . . . . . . . . . . . . . . 17
ā¢ (((š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā§ (š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā§ (š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ))) ā ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ)))) |
5 | | poirr 5601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
ā¢ ((š
Po š“ ā§ š ā š“) ā Ā¬ šš
š) |
6 | 5 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
ā¢ (š
Po š“ ā (š ā š“ ā Ā¬ šš
š)) |
7 | | poirr 5601 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
ā¢ ((š Po šµ ā§ š ā šµ) ā Ā¬ ššš) |
8 | 7 | intnand 487 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
ā¢ ((š Po šµ ā§ š ā šµ) ā Ā¬ (š = š ā§ ššš)) |
9 | 8 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
ā¢ (š Po šµ ā (š ā šµ ā Ā¬ (š = š ā§ ššš))) |
10 | 6, 9 | im2anan9 618 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ā¢ ((š
Po š“ ā§ š Po šµ) ā ((š ā š“ ā§ š ā šµ) ā (Ā¬ šš
š ā§ Ā¬ (š = š ā§ ššš)))) |
11 | | ioran 980 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ā¢ (Ā¬
(šš
š āØ (š = š ā§ ššš)) ā (Ā¬ šš
š ā§ Ā¬ (š = š ā§ ššš))) |
12 | 10, 11 | imbitrrdi 251 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢ ((š
Po š“ ā§ š Po šµ) ā ((š ā š“ ā§ š ā šµ) ā Ā¬ (šš
š āØ (š = š ā§ ššš)))) |
13 | 12 | imp 405 |
. . . . . . . . . . . . . . . . . . . . . . 23
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ (š ā š“ ā§ š ā šµ)) ā Ā¬ (šš
š āØ (š = š ā§ ššš))) |
14 | 13 | intnand 487 |
. . . . . . . . . . . . . . . . . . . . . 22
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ (š ā š“ ā§ š ā šµ)) ā Ā¬ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) |
15 | 14 | 3ad2antr1 1186 |
. . . . . . . . . . . . . . . . . . . . 21
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā Ā¬ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) |
16 | | an4 652 |
. . . . . . . . . . . . . . . . . . . . . 22
ā¢
(((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) ā ((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ ((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ))) ā§ ((šš
š āØ (š = š ā§ ššš)) ā§ (šš
š āØ (š = š ā§ ššš))))) |
17 | | 3an6 1444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ā¢ (((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ)) ā ((š ā š“ ā§ š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ))) |
18 | | potr 5602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
ā¢ ((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“)) ā ((šš
š ā§ šš
š) ā šš
š)) |
19 | 18 | 3impia 1115 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
ā¢ ((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“) ā§ (šš
š ā§ šš
š)) ā šš
š) |
20 | 19 | orcd 869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
ā¢ ((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“) ā§ (šš
š ā§ šš
š)) ā (šš
š āØ (š = š ā§ ššš))) |
21 | 20 | 3expia 1119 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
ā¢ ((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“)) ā ((šš
š ā§ šš
š) ā (šš
š āØ (š = š ā§ ššš)))) |
22 | 21 | expdimp 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ā¢ (((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“)) ā§ šš
š) ā (šš
š ā (šš
š āØ (š = š ā§ ššš)))) |
23 | | breq2 5153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
ā¢ (š = š ā (šš
š ā šš
š)) |
24 | 23 | biimpa 475 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
ā¢ ((š = š ā§ šš
š) ā šš
š) |
25 | 24 | orcd 869 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
ā¢ ((š = š ā§ šš
š) ā (šš
š āØ (š = š ā§ ššš))) |
26 | 25 | expcom 412 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
ā¢ (šš
š ā (š = š ā (šš
š āØ (š = š ā§ ššš)))) |
27 | 26 | adantrd 490 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
ā¢ (šš
š ā ((š = š ā§ ššš) ā (šš
š āØ (š = š ā§ ššš)))) |
28 | 27 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ā¢ (((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“)) ā§ šš
š) ā ((š = š ā§ ššš) ā (šš
š āØ (š = š ā§ ššš)))) |
29 | 22, 28 | jaod 855 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ā¢ (((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“)) ā§ šš
š) ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš)))) |
30 | 29 | ex 411 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
ā¢ ((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“)) ā (šš
š ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš))))) |
31 | | potr 5602 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
ā¢ ((š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ)) ā ((ššš ā§ ššš) ā ššš)) |
32 | 31 | expdimp 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
ā¢ (((š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ)) ā§ ššš) ā (ššš ā ššš)) |
33 | 32 | anim2d 610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
ā¢ (((š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ)) ā§ ššš) ā ((š = š ā§ ššš) ā (š = š ā§ ššš))) |
34 | 33 | orim2d 963 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
ā¢ (((š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ)) ā§ ššš) ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš)))) |
35 | | breq1 5152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
ā¢ (š = š ā (šš
š ā šš
š)) |
36 | | equequ1 2026 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
ā¢ (š = š ā (š = š ā š = š)) |
37 | 36 | anbi1d 628 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
ā¢ (š = š ā ((š = š ā§ ššš) ā (š = š ā§ ššš))) |
38 | 35, 37 | orbi12d 915 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
ā¢ (š = š ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš)))) |
39 | 38 | imbi2d 339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
ā¢ (š = š ā (((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš))) ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš))))) |
40 | 34, 39 | imbitrrid 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
ā¢ (š = š ā (((š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ)) ā§ ššš) ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš))))) |
41 | 40 | expd 414 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
ā¢ (š = š ā ((š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ)) ā (ššš ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš)))))) |
42 | 41 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
ā¢ ((š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ)) ā (š = š ā (ššš ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš)))))) |
43 | 42 | impd 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
ā¢ ((š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ)) ā ((š = š ā§ ššš) ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš))))) |
44 | 30, 43 | jaao 951 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
ā¢ (((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“)) ā§ (š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ))) ā ((šš
š āØ (š = š ā§ ššš)) ā ((šš
š āØ (š = š ā§ ššš)) ā (šš
š āØ (š = š ā§ ššš))))) |
45 | 44 | impd 409 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
ā¢ (((š
Po š“ ā§ (š ā š“ ā§ š ā š“ ā§ š ā š“)) ā§ (š Po šµ ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ))) ā (((šš
š āØ (š = š ā§ ššš)) ā§ (šš
š āØ (š = š ā§ ššš))) ā (šš
š āØ (š = š ā§ ššš)))) |
46 | 45 | an4s 656 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ ā§ š ā šµ))) ā (((šš
š āØ (š = š ā§ ššš)) ā§ (šš
š āØ (š = š ā§ ššš))) ā (šš
š āØ (š = š ā§ ššš)))) |
47 | 17, 46 | sylan2b 592 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā (((šš
š āØ (š = š ā§ ššš)) ā§ (šš
š āØ (š = š ā§ ššš))) ā (šš
š āØ (š = š ā§ ššš)))) |
48 | | an4 652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
ā¢ (((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ)) ā ((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ))) |
49 | 48 | biimpi 215 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
ā¢ (((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ)) ā ((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ))) |
50 | 49 | 3adant2 1129 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ā¢ (((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ)) ā ((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ))) |
51 | 50 | adantl 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā ((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ))) |
52 | 47, 51 | jctild 524 |
. . . . . . . . . . . . . . . . . . . . . . 23
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā (((šš
š āØ (š = š ā§ ššš)) ā§ (šš
š āØ (š = š ā§ ššš))) ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))))) |
53 | 52 | adantld 489 |
. . . . . . . . . . . . . . . . . . . . . 22
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā (((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ ((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ))) ā§ ((šš
š āØ (š = š ā§ ššš)) ā§ (šš
š āØ (š = š ā§ ššš)))) ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))))) |
54 | 16, 53 | biimtrid 241 |
. . . . . . . . . . . . . . . . . . . . 21
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā (((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))))) |
55 | 15, 54 | jca 510 |
. . . . . . . . . . . . . . . . . . . 20
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā (Ā¬ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))))) |
56 | | breq12 5154 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ā¢ ((š” = āØš, šā© ā§ š” = āØš, šā©) ā (š”šš” ā āØš, šā©šāØš, šā©)) |
57 | 56 | anidms 565 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢ (š” = āØš, šā© ā (š”šš” ā āØš, šā©šāØš, šā©)) |
58 | 57 | notbid 317 |
. . . . . . . . . . . . . . . . . . . . . . 23
ā¢ (š” = āØš, šā© ā (Ā¬ š”šš” ā Ā¬ āØš, šā©šāØš, šā©)) |
59 | 58 | 3ad2ant1 1131 |
. . . . . . . . . . . . . . . . . . . . . 22
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā (Ā¬ š”šš” ā Ā¬ āØš, šā©šāØš, šā©)) |
60 | | breq12 5154 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā©) ā (š”šš¢ ā āØš, šā©šāØš, šā©)) |
61 | 60 | 3adant3 1130 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā (š”šš¢ ā āØš, šā©šāØš, šā©)) |
62 | | breq12 5154 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
ā¢ ((š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā (š¢šš£ ā āØš, šā©šāØš, šā©)) |
63 | 62 | 3adant1 1128 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā (š¢šš£ ā āØš, šā©šāØš, šā©)) |
64 | 61, 63 | anbi12d 629 |
. . . . . . . . . . . . . . . . . . . . . . 23
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā ((š”šš¢ ā§ š¢šš£) ā (āØš, šā©šāØš, šā© ā§ āØš, šā©šāØš, šā©))) |
65 | | breq12 5154 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢ ((š” = āØš, šā© ā§ š£ = āØš, šā©) ā (š”šš£ ā āØš, šā©šāØš, šā©)) |
66 | 65 | 3adant2 1129 |
. . . . . . . . . . . . . . . . . . . . . . 23
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā (š”šš£ ā āØš, šā©šāØš, šā©)) |
67 | 64, 66 | imbi12d 343 |
. . . . . . . . . . . . . . . . . . . . . 22
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā (((š”šš¢ ā§ š¢šš£) ā š”šš£) ā ((āØš, šā©šāØš, šā© ā§ āØš, šā©šāØš, šā©) ā āØš, šā©šāØš, šā©))) |
68 | 59, 67 | anbi12d 629 |
. . . . . . . . . . . . . . . . . . . . 21
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā ((Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)) ā (Ā¬ āØš, šā©šāØš, šā© ā§ ((āØš, šā©šāØš, šā© ā§ āØš, šā©šāØš, šā©) ā āØš, šā©šāØš, šā©)))) |
69 | | poxp.1 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢ š = {āØš„, š¦ā© ā£ ((š„ ā (š“ Ć šµ) ā§ š¦ ā (š“ Ć šµ)) ā§ ((1st āš„)š
(1st āš¦) āØ ((1st āš„) = (1st āš¦) ā§ (2nd
āš„)š(2nd āš¦))))} |
70 | 69 | xporderlem 8117 |
. . . . . . . . . . . . . . . . . . . . . . 23
ā¢
(āØš, šā©šāØš, šā© ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) |
71 | 70 | notbii 319 |
. . . . . . . . . . . . . . . . . . . . . 22
ā¢ (Ā¬
āØš, šā©šāØš, šā© ā Ā¬ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) |
72 | 69 | xporderlem 8117 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢
(āØš, šā©šāØš, šā© ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) |
73 | 69 | xporderlem 8117 |
. . . . . . . . . . . . . . . . . . . . . . . 24
ā¢
(āØš, šā©šāØš, šā© ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) |
74 | 72, 73 | anbi12i 625 |
. . . . . . . . . . . . . . . . . . . . . . 23
ā¢
((āØš, šā©šāØš, šā© ā§ āØš, šā©šāØš, šā©) ā ((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))))) |
75 | 69 | xporderlem 8117 |
. . . . . . . . . . . . . . . . . . . . . . 23
ā¢
(āØš, šā©šāØš, šā© ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) |
76 | 74, 75 | imbi12i 349 |
. . . . . . . . . . . . . . . . . . . . . 22
ā¢
(((āØš, šā©šāØš, šā© ā§ āØš, šā©šāØš, šā©) ā āØš, šā©šāØš, šā©) ā (((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))))) |
77 | 71, 76 | anbi12i 625 |
. . . . . . . . . . . . . . . . . . . . 21
ā¢ ((Ā¬
āØš, šā©šāØš, šā© ā§ ((āØš, šā©šāØš, šā© ā§ āØš, šā©šāØš, šā©) ā āØš, šā©šāØš, šā©)) ā (Ā¬ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))))) |
78 | 68, 77 | bitrdi 286 |
. . . . . . . . . . . . . . . . . . . 20
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā ((Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)) ā (Ā¬ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))) ā§ (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš)))) ā (((š ā š“ ā§ š ā š“) ā§ (š ā šµ ā§ š ā šµ)) ā§ (šš
š āØ (š = š ā§ ššš))))))) |
79 | 55, 78 | imbitrrid 245 |
. . . . . . . . . . . . . . . . . . 19
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā (((š
Po š“ ā§ š Po šµ) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))) |
80 | 79 | expcomd 415 |
. . . . . . . . . . . . . . . . . 18
ā¢ ((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā (((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£))))) |
81 | 80 | imp 405 |
. . . . . . . . . . . . . . . . 17
ā¢ (((š” = āØš, šā© ā§ š¢ = āØš, šā© ā§ š£ = āØš, šā©) ā§ ((š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ) ā§ (š ā š“ ā§ š ā šµ))) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))) |
82 | 4, 81 | sylbi 216 |
. . . . . . . . . . . . . . . 16
ā¢ (((š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā§ (š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā§ (š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ))) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))) |
83 | 82 | 3exp 1117 |
. . . . . . . . . . . . . . 15
ā¢ ((š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))))) |
84 | 83 | com3l 89 |
. . . . . . . . . . . . . 14
ā¢ ((š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))))) |
85 | 84 | exlimivv 1933 |
. . . . . . . . . . . . 13
ā¢
(āšāš(š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))))) |
86 | 85 | com3l 89 |
. . . . . . . . . . . 12
ā¢ ((š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā (āšāš(š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))))) |
87 | 86 | exlimivv 1933 |
. . . . . . . . . . 11
ā¢
(āšāš(š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā (āšāš(š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))))) |
88 | 87 | com3l 89 |
. . . . . . . . . 10
ā¢ ((š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā (āšāš(š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā (āšāš(š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))))) |
89 | 88 | exlimivv 1933 |
. . . . . . . . 9
ā¢
(āšāš(š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā (āšāš(š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā (āšāš(š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))))) |
90 | 89 | 3imp 1109 |
. . . . . . . 8
ā¢
((āšāš(š” = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā§ āšāš(š¢ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ)) ā§ āšāš(š£ = āØš, šā© ā§ (š ā š“ ā§ š ā šµ))) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))) |
91 | 1, 2, 3, 90 | syl3anb 1159 |
. . . . . . 7
ā¢ ((š” ā (š“ Ć šµ) ā§ š¢ ā (š“ Ć šµ) ā§ š£ ā (š“ Ć šµ)) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))) |
92 | 91 | 3expia 1119 |
. . . . . 6
ā¢ ((š” ā (š“ Ć šµ) ā§ š¢ ā (š“ Ć šµ)) ā (š£ ā (š“ Ć šµ) ā ((š
Po š“ ā§ š Po šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£))))) |
93 | 92 | com3r 87 |
. . . . 5
ā¢ ((š
Po š“ ā§ š Po šµ) ā ((š” ā (š“ Ć šµ) ā§ š¢ ā (š“ Ć šµ)) ā (š£ ā (š“ Ć šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£))))) |
94 | 93 | imp 405 |
. . . 4
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ (š” ā (š“ Ć šµ) ā§ š¢ ā (š“ Ć šµ))) ā (š£ ā (š“ Ć šµ) ā (Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£)))) |
95 | 94 | ralrimiv 3143 |
. . 3
ā¢ (((š
Po š“ ā§ š Po šµ) ā§ (š” ā (š“ Ć šµ) ā§ š¢ ā (š“ Ć šµ))) ā āš£ ā (š“ Ć šµ)(Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£))) |
96 | 95 | ralrimivva 3198 |
. 2
ā¢ ((š
Po š“ ā§ š Po šµ) ā āš” ā (š“ Ć šµ)āš¢ ā (š“ Ć šµ)āš£ ā (š“ Ć šµ)(Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£))) |
97 | | df-po 5589 |
. 2
ā¢ (š Po (š“ Ć šµ) ā āš” ā (š“ Ć šµ)āš¢ ā (š“ Ć šµ)āš£ ā (š“ Ć šµ)(Ā¬ š”šš” ā§ ((š”šš¢ ā§ š¢šš£) ā š”šš£))) |
98 | 96, 97 | sylibr 233 |
1
ā¢ ((š
Po š“ ā§ š Po šµ) ā š Po (š“ Ć šµ)) |