Step | Hyp | Ref
| Expression |
1 | | idn1 42948 |
. . . . . . . . . . . . . 14
⢠( đ´ â đľ âś đ´ â đľ ) |
2 | | sbcg 3822 |
. . . . . . . . . . . . . . 15
⢠(đ´ â đľ â ([đ´ / đĽ]đ§ â đŚ â đ§ â đŚ)) |
3 | 1, 2 | e1a 43001 |
. . . . . . . . . . . . . 14
⢠( đ´ â đľ âś ([đ´ / đĽ]đ§ â đŚ â đ§ â đŚ) ) |
4 | | sbcel2gv 3815 |
. . . . . . . . . . . . . . 15
⢠(đ´ â đľ â ([đ´ / đĽ]đŚ â đĽ â đŚ â đ´)) |
5 | 1, 4 | e1a 43001 |
. . . . . . . . . . . . . 14
⢠( đ´ â đľ âś ([đ´ / đĽ]đŚ â đĽ â đŚ â đ´) ) |
6 | | sbcel2gv 3815 |
. . . . . . . . . . . . . . 15
⢠(đ´ â đľ â ([đ´ / đĽ]đ§ â đĽ â đ§ â đ´)) |
7 | 1, 6 | e1a 43001 |
. . . . . . . . . . . . . 14
⢠( đ´ â đľ âś ([đ´ / đĽ]đ§ â đĽ â đ§ â đ´) ) |
8 | | imbi13 42894 |
. . . . . . . . . . . . . . 15
â˘
(([đ´ / đĽ]đ§ â đŚ â đ§ â đŚ) â (([đ´ / đĽ]đŚ â đĽ â đŚ â đ´) â (([đ´ / đĽ]đ§ â đĽ â đ§ â đ´) â (([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´)))))) |
9 | 8 | a1i 11 |
. . . . . . . . . . . . . 14
⢠(đ´ â đľ â (([đ´ / đĽ]đ§ â đŚ â đ§ â đŚ) â (([đ´ / đĽ]đŚ â đĽ â đŚ â đ´) â (([đ´ / đĽ]đ§ â đĽ â đ§ â đ´) â (([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))))))) |
10 | 1, 3, 5, 7, 9 | e1111 43049 |
. . . . . . . . . . . . 13
⢠( đ´ â đľ âś (([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))) ) |
11 | | sbcim2g 42912 |
. . . . . . . . . . . . . 14
⢠(đ´ â đľ â ([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ)))) |
12 | 1, 11 | e1a 43001 |
. . . . . . . . . . . . 13
⢠( đ´ â đľ âś ([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ))) ) |
13 | | bibi1 352 |
. . . . . . . . . . . . . 14
â˘
(([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ))) â (([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))) â (([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))))) |
14 | 13 | biimprcd 250 |
. . . . . . . . . . . . 13
â˘
((([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))) â (([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ([đ´ / đĽ]đ§ â đŚ â ([đ´ / đĽ]đŚ â đĽ â [đ´ / đĽ]đ§ â đĽ))) â ([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))))) |
15 | 10, 12, 14 | e11 43062 |
. . . . . . . . . . . 12
⢠( đ´ â đľ âś ([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))) ) |
16 | | pm3.31 451 |
. . . . . . . . . . . . 13
⢠((đ§ â đŚ â (đŚ â đ´ â đ§ â đ´)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) |
17 | | pm3.3 450 |
. . . . . . . . . . . . 13
⢠(((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))) |
18 | 16, 17 | impbii 208 |
. . . . . . . . . . . 12
⢠((đ§ â đŚ â (đŚ â đ´ â đ§ â đ´)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) |
19 | | bibi1 352 |
. . . . . . . . . . . . 13
â˘
(([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))) â (([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â ((đ§ â đŚ â (đŚ â đ´ â đ§ â đ´)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)))) |
20 | 19 | biimprd 248 |
. . . . . . . . . . . 12
â˘
(([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â (đ§ â đŚ â (đŚ â đ´ â đ§ â đ´))) â (((đ§ â đŚ â (đŚ â đ´ â đ§ â đ´)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â ([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)))) |
21 | 15, 18, 20 | e10 43068 |
. . . . . . . . . . 11
⢠( đ´ â đľ âś ([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ) |
22 | | pm3.31 451 |
. . . . . . . . . . . . . 14
⢠((đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) |
23 | | pm3.3 450 |
. . . . . . . . . . . . . 14
⢠(((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â (đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ))) |
24 | 22, 23 | impbii 208 |
. . . . . . . . . . . . 13
⢠((đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) |
25 | 24 | ax-gen 1798 |
. . . . . . . . . . . 12
â˘
âđĽ((đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) |
26 | | sbcbi 42913 |
. . . . . . . . . . . 12
⢠(đ´ â đľ â (âđĽ((đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â ([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â [đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)))) |
27 | 1, 25, 26 | e10 43068 |
. . . . . . . . . . 11
⢠( đ´ â đľ âś ([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â [đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) ) |
28 | | bitr3 353 |
. . . . . . . . . . . 12
â˘
(([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â [đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â (([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â ([đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)))) |
29 | 28 | com12 32 |
. . . . . . . . . . 11
â˘
(([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â (([đ´ / đĽ](đ§ â đŚ â (đŚ â đĽ â đ§ â đĽ)) â [đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â ([đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)))) |
30 | 21, 27, 29 | e11 43062 |
. . . . . . . . . 10
⢠( đ´ â đľ âś ([đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ) |
31 | 30 | gen11 42990 |
. . . . . . . . 9
⢠( đ´ â đľ âś âđŚ([đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ) |
32 | | albi 1821 |
. . . . . . . . 9
â˘
(âđŚ([đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â (âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´))) |
33 | 31, 32 | e1a 43001 |
. . . . . . . 8
⢠( đ´ â đľ âś (âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ) |
34 | | sbcal 3807 |
. . . . . . . . . 10
â˘
([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) |
35 | 34 | a1i 11 |
. . . . . . . . 9
⢠(đ´ â đľ â ([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ))) |
36 | 1, 35 | e1a 43001 |
. . . . . . . 8
⢠( đ´ â đľ âś ([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) ) |
37 | | bibi1 352 |
. . . . . . . . 9
â˘
(([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â (([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â (âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)))) |
38 | 37 | biimprcd 250 |
. . . . . . . 8
â˘
((âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â (([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ[đ´ / đĽ]((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â ([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)))) |
39 | 33, 36, 38 | e11 43062 |
. . . . . . 7
⢠( đ´ â đľ âś ([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ) |
40 | 39 | gen11 42990 |
. . . . . 6
⢠( đ´ â đľ âś âđ§([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ) |
41 | | albi 1821 |
. . . . . 6
â˘
(âđ§([đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â (âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´))) |
42 | 40, 41 | e1a 43001 |
. . . . 5
⢠( đ´ â đľ âś (âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ) |
43 | | sbcal 3807 |
. . . . . . 7
â˘
([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) |
44 | 43 | a1i 11 |
. . . . . 6
⢠(đ´ â đľ â ([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ))) |
45 | 1, 44 | e1a 43001 |
. . . . 5
⢠( đ´ â đľ âś ([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) ) |
46 | | bibi1 352 |
. . . . . 6
â˘
(([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â (([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â (âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)))) |
47 | 46 | biimprcd 250 |
. . . . 5
â˘
((âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â (([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§[đ´ / đĽ]âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â ([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)))) |
48 | 42, 45, 47 | e11 43062 |
. . . 4
⢠( đ´ â đľ âś ([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ) |
49 | | dftr2 5228 |
. . . 4
⢠(Tr đ´ â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) |
50 | | biantr 805 |
. . . . 5
â˘
((([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) ⧠(Tr đ´ â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´))) â ([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â Tr đ´)) |
51 | 50 | ex 414 |
. . . 4
â˘
(([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â ((Tr đ´ â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đ´) â đ§ â đ´)) â ([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â Tr đ´))) |
52 | 48, 49, 51 | e10 43068 |
. . 3
⢠( đ´ â đľ âś ([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â Tr đ´) ) |
53 | | dftr2 5228 |
. . . . 5
⢠(Tr đĽ â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) |
54 | 53 | ax-gen 1798 |
. . . 4
â˘
âđĽ(Tr đĽ â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) |
55 | | sbcbi 42913 |
. . . 4
⢠(đ´ â đľ â (âđĽ(Tr đĽ â âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â ([đ´ / đĽ]Tr đĽ â [đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)))) |
56 | 1, 54, 55 | e10 43068 |
. . 3
⢠( đ´ â đľ âś ([đ´ / đĽ]Tr đĽ â [đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) ) |
57 | | bibi1 352 |
. . . 4
â˘
(([đ´ / đĽ]Tr đĽ â [đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â (([đ´ / đĽ]Tr đĽ â Tr đ´) â ([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â Tr đ´))) |
58 | 57 | biimprcd 250 |
. . 3
â˘
(([đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ) â Tr đ´) â (([đ´ / đĽ]Tr đĽ â [đ´ / đĽ]âđ§âđŚ((đ§ â đŚ ⧠đŚ â đĽ) â đ§ â đĽ)) â ([đ´ / đĽ]Tr đĽ â Tr đ´))) |
59 | 52, 56, 58 | e11 43062 |
. 2
⢠( đ´ â đľ âś ([đ´ / đĽ]Tr đĽ â Tr đ´) ) |
60 | 59 | in1 42945 |
1
⢠(đ´ â đľ â ([đ´ / đĽ]Tr đĽ â Tr đ´)) |