Step | Hyp | Ref
| Expression |
1 | | cnre 7952 |
. . 3
โข (๐ถ โ โ โ
โ๐ข โ โ
โ๐ฃ โ โ
๐ถ = (๐ข + (i ยท ๐ฃ))) |
2 | 1 | 3ad2ant3 1020 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
โ๐ข โ โ
โ๐ฃ โ โ
๐ถ = (๐ข + (i ยท ๐ฃ))) |
3 | | cnre 7952 |
. . . . . . 7
โข (๐ต โ โ โ
โ๐ง โ โ
โ๐ค โ โ
๐ต = (๐ง + (i ยท ๐ค))) |
4 | 3 | 3ad2ant2 1019 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
โ๐ง โ โ
โ๐ค โ โ
๐ต = (๐ง + (i ยท ๐ค))) |
5 | 4 | ad2antrr 488 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โ โ๐ง โ โ โ๐ค โ โ ๐ต = (๐ง + (i ยท ๐ค))) |
6 | | cnre 7952 |
. . . . . . . . . . 11
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |
7 | 6 | 3ad2ant1 1018 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |
8 | 7 | adantr 276 |
. . . . . . . . 9
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โ
โ๐ฅ โ โ
โ๐ฆ โ โ
๐ด = (๐ฅ + (i ยท ๐ฆ))) |
9 | 8 | ad3antrrr 492 |
. . . . . . . 8
โข
((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ โ๐ฅ โ โ โ๐ฆ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) |
10 | | simpr 110 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ด = (๐ฅ + (i ยท ๐ฆ))) |
11 | | simpllr 534 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ต = (๐ง + (i ยท ๐ค))) |
12 | 10, 11 | breq12d 4016 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด # ๐ต โ (๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)))) |
13 | | simplrl 535 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ฅ โ โ) |
14 | | simplrr 536 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ฆ โ โ) |
15 | | simprl 529 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โ ๐ง โ โ) |
16 | 15 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ง โ โ) |
17 | | simprr 531 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โ ๐ค โ โ) |
18 | 17 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ค โ โ) |
19 | | apreim 8559 |
. . . . . . . . . . . . . . 15
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ง โ โ โง ๐ค โ โ)) โ ((๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)) โ (๐ฅ # ๐ง โจ ๐ฆ # ๐ค))) |
20 | 13, 14, 16, 18, 19 | syl22anc 1239 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ฅ + (i ยท ๐ฆ)) # (๐ง + (i ยท ๐ค)) โ (๐ฅ # ๐ง โจ ๐ฆ # ๐ค))) |
21 | 12, 20 | bitrd 188 |
. . . . . . . . . . . . 13
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด # ๐ต โ (๐ฅ # ๐ง โจ ๐ฆ # ๐ค))) |
22 | | simprl 529 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โ ๐ข โ
โ) |
23 | 22 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โ ๐ข โ โ) |
24 | 23 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ข โ โ) |
25 | | reapcotr 8554 |
. . . . . . . . . . . . . . 15
โข ((๐ฅ โ โ โง ๐ง โ โ โง ๐ข โ โ) โ (๐ฅ # ๐ง โ (๐ฅ # ๐ข โจ ๐ง # ๐ข))) |
26 | 13, 16, 24, 25 | syl3anc 1238 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ฅ # ๐ง โ (๐ฅ # ๐ข โจ ๐ง # ๐ข))) |
27 | | simprr 531 |
. . . . . . . . . . . . . . . . 17
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โ ๐ฃ โ
โ) |
28 | 27 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โ ๐ฃ โ โ) |
29 | 28 | ad3antrrr 492 |
. . . . . . . . . . . . . . 15
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ฃ โ โ) |
30 | | reapcotr 8554 |
. . . . . . . . . . . . . . 15
โข ((๐ฆ โ โ โง ๐ค โ โ โง ๐ฃ โ โ) โ (๐ฆ # ๐ค โ (๐ฆ # ๐ฃ โจ ๐ค # ๐ฃ))) |
31 | 14, 18, 29, 30 | syl3anc 1238 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ฆ # ๐ค โ (๐ฆ # ๐ฃ โจ ๐ค # ๐ฃ))) |
32 | 26, 31 | orim12d 786 |
. . . . . . . . . . . . 13
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ฅ # ๐ง โจ ๐ฆ # ๐ค) โ ((๐ฅ # ๐ข โจ ๐ง # ๐ข) โจ (๐ฆ # ๐ฃ โจ ๐ค # ๐ฃ)))) |
33 | 21, 32 | sylbid 150 |
. . . . . . . . . . . 12
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด # ๐ต โ ((๐ฅ # ๐ข โจ ๐ง # ๐ข) โจ (๐ฆ # ๐ฃ โจ ๐ค # ๐ฃ)))) |
34 | | or4 771 |
. . . . . . . . . . . 12
โข (((๐ฅ # ๐ข โจ ๐ง # ๐ข) โจ (๐ฆ # ๐ฃ โจ ๐ค # ๐ฃ)) โ ((๐ฅ # ๐ข โจ ๐ฆ # ๐ฃ) โจ (๐ง # ๐ข โจ ๐ค # ๐ฃ))) |
35 | 33, 34 | imbitrdi 161 |
. . . . . . . . . . 11
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด # ๐ต โ ((๐ฅ # ๐ข โจ ๐ฆ # ๐ฃ) โจ (๐ง # ๐ข โจ ๐ค # ๐ฃ)))) |
36 | | simplr 528 |
. . . . . . . . . . . . . . 15
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โ ๐ถ = (๐ข + (i ยท ๐ฃ))) |
37 | 36 | ad3antrrr 492 |
. . . . . . . . . . . . . 14
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ๐ถ = (๐ข + (i ยท ๐ฃ))) |
38 | 10, 37 | breq12d 4016 |
. . . . . . . . . . . . 13
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด # ๐ถ โ (๐ฅ + (i ยท ๐ฆ)) # (๐ข + (i ยท ๐ฃ)))) |
39 | | apreim 8559 |
. . . . . . . . . . . . . 14
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โ ((๐ฅ + (i ยท ๐ฆ)) # (๐ข + (i ยท ๐ฃ)) โ (๐ฅ # ๐ข โจ ๐ฆ # ๐ฃ))) |
40 | 13, 14, 24, 29, 39 | syl22anc 1239 |
. . . . . . . . . . . . 13
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ฅ + (i ยท ๐ฆ)) # (๐ข + (i ยท ๐ฃ)) โ (๐ฅ # ๐ข โจ ๐ฆ # ๐ฃ))) |
41 | 38, 40 | bitrd 188 |
. . . . . . . . . . . 12
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด # ๐ถ โ (๐ฅ # ๐ข โจ ๐ฆ # ๐ฃ))) |
42 | 11, 37 | breq12d 4016 |
. . . . . . . . . . . . 13
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ต # ๐ถ โ (๐ง + (i ยท ๐ค)) # (๐ข + (i ยท ๐ฃ)))) |
43 | | apreim 8559 |
. . . . . . . . . . . . . 14
โข (((๐ง โ โ โง ๐ค โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โ ((๐ง + (i ยท ๐ค)) # (๐ข + (i ยท ๐ฃ)) โ (๐ง # ๐ข โจ ๐ค # ๐ฃ))) |
44 | 16, 18, 24, 29, 43 | syl22anc 1239 |
. . . . . . . . . . . . 13
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ง + (i ยท ๐ค)) # (๐ข + (i ยท ๐ฃ)) โ (๐ง # ๐ข โจ ๐ค # ๐ฃ))) |
45 | 42, 44 | bitrd 188 |
. . . . . . . . . . . 12
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ต # ๐ถ โ (๐ง # ๐ข โจ ๐ค # ๐ฃ))) |
46 | 41, 45 | orbi12d 793 |
. . . . . . . . . . 11
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ ((๐ด # ๐ถ โจ ๐ต # ๐ถ) โ ((๐ฅ # ๐ข โจ ๐ฆ # ๐ฃ) โจ (๐ง # ๐ข โจ ๐ค # ๐ฃ)))) |
47 | 35, 46 | sylibrd 169 |
. . . . . . . . . 10
โข
((((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ด = (๐ฅ + (i ยท ๐ฆ))) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ))) |
48 | 47 | ex 115 |
. . . . . . . . 9
โข
(((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ)))) |
49 | 48 | rexlimdvva 2602 |
. . . . . . . 8
โข
((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (โ๐ฅ โ โ โ๐ฆ โ โ ๐ด = (๐ฅ + (i ยท ๐ฆ)) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ)))) |
50 | 9, 49 | mpd 13 |
. . . . . . 7
โข
((((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โง ๐ต = (๐ง + (i ยท ๐ค))) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ))) |
51 | 50 | ex 115 |
. . . . . 6
โข
(((((๐ด โ
โ โง ๐ต โ
โ โง ๐ถ โ
โ) โง (๐ข โ
โ โง ๐ฃ โ
โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โง (๐ง โ โ โง ๐ค โ โ)) โ (๐ต = (๐ง + (i ยท ๐ค)) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ)))) |
52 | 51 | rexlimdvva 2602 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โ (โ๐ง โ โ โ๐ค โ โ ๐ต = (๐ง + (i ยท ๐ค)) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ)))) |
53 | 5, 52 | mpd 13 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โง ๐ถ = (๐ข + (i ยท ๐ฃ))) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ))) |
54 | 53 | ex 115 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โง (๐ข โ โ โง ๐ฃ โ โ)) โ (๐ถ = (๐ข + (i ยท ๐ฃ)) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ)))) |
55 | 54 | rexlimdvva 2602 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ
(โ๐ข โ โ
โ๐ฃ โ โ
๐ถ = (๐ข + (i ยท ๐ฃ)) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ)))) |
56 | 2, 55 | mpd 13 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด # ๐ต โ (๐ด # ๐ถ โจ ๐ต # ๐ถ))) |