Step | Hyp | Ref
| Expression |
1 | | simpll 766 |
. . . 4
โข
(((((๐ด โ
โ โง 0 โค ๐ด)
โง ๐ต โ โ)
โง ((๐ถ โ โ
โง 0 โค ๐ถ) โง ๐ท โ โ)) โง (๐ด โค ๐ต โง ๐ถ โค ๐ท)) โ ((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ)) |
2 | | simpll 766 |
. . . . 5
โข (((๐ถ โ โ โง 0 โค
๐ถ) โง ๐ท โ โ) โ ๐ถ โ โ) |
3 | 2 | ad2antlr 726 |
. . . 4
โข
(((((๐ด โ
โ โง 0 โค ๐ด)
โง ๐ต โ โ)
โง ((๐ถ โ โ
โง 0 โค ๐ถ) โง ๐ท โ โ)) โง (๐ด โค ๐ต โง ๐ถ โค ๐ท)) โ ๐ถ โ โ) |
4 | | simplrr 777 |
. . . . 5
โข
(((((๐ด โ
โ โง 0 โค ๐ด)
โง ๐ต โ โ)
โง ((๐ถ โ โ
โง 0 โค ๐ถ) โง ๐ท โ โ)) โง (๐ด โค ๐ต โง ๐ถ โค ๐ท)) โ ๐ท โ โ) |
5 | | 0re 11165 |
. . . . . . . . . 10
โข 0 โ
โ |
6 | | letr 11257 |
. . . . . . . . . 10
โข ((0
โ โ โง ๐ถ
โ โ โง ๐ท
โ โ) โ ((0 โค ๐ถ โง ๐ถ โค ๐ท) โ 0 โค ๐ท)) |
7 | 5, 6 | mp3an1 1449 |
. . . . . . . . 9
โข ((๐ถ โ โ โง ๐ท โ โ) โ ((0 โค
๐ถ โง ๐ถ โค ๐ท) โ 0 โค ๐ท)) |
8 | 7 | exp4b 432 |
. . . . . . . 8
โข (๐ถ โ โ โ (๐ท โ โ โ (0 โค
๐ถ โ (๐ถ โค ๐ท โ 0 โค ๐ท)))) |
9 | 8 | com23 86 |
. . . . . . 7
โข (๐ถ โ โ โ (0 โค
๐ถ โ (๐ท โ โ โ (๐ถ โค ๐ท โ 0 โค ๐ท)))) |
10 | 9 | imp41 427 |
. . . . . 6
โข ((((๐ถ โ โ โง 0 โค
๐ถ) โง ๐ท โ โ) โง ๐ถ โค ๐ท) โ 0 โค ๐ท) |
11 | 10 | ad2ant2l 745 |
. . . . 5
โข
(((((๐ด โ
โ โง 0 โค ๐ด)
โง ๐ต โ โ)
โง ((๐ถ โ โ
โง 0 โค ๐ถ) โง ๐ท โ โ)) โง (๐ด โค ๐ต โง ๐ถ โค ๐ท)) โ 0 โค ๐ท) |
12 | 4, 11 | jca 513 |
. . . 4
โข
(((((๐ด โ
โ โง 0 โค ๐ด)
โง ๐ต โ โ)
โง ((๐ถ โ โ
โง 0 โค ๐ถ) โง ๐ท โ โ)) โง (๐ด โค ๐ต โง ๐ถ โค ๐ท)) โ (๐ท โ โ โง 0 โค ๐ท)) |
13 | 1, 3, 12 | jca32 517 |
. . 3
โข
(((((๐ด โ
โ โง 0 โค ๐ด)
โง ๐ต โ โ)
โง ((๐ถ โ โ
โง 0 โค ๐ถ) โง ๐ท โ โ)) โง (๐ด โค ๐ต โง ๐ถ โค ๐ท)) โ (((๐ด โ โ โง 0 โค ๐ด) โง ๐ต โ โ) โง (๐ถ โ โ โง (๐ท โ โ โง 0 โค ๐ท)))) |
14 | | simpr 486 |
. . 3
โข
(((((๐ด โ
โ โง 0 โค ๐ด)
โง ๐ต โ โ)
โง ((๐ถ โ โ
โง 0 โค ๐ถ) โง ๐ท โ โ)) โง (๐ด โค ๐ต โง ๐ถ โค ๐ท)) โ (๐ด โค ๐ต โง ๐ถ โค ๐ท)) |
15 | | lemul12b 12020 |
. . 3
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ) โง (๐ถ โ โ โง (๐ท โ โ โง 0 โค ๐ท))) โ ((๐ด โค ๐ต โง ๐ถ โค ๐ท) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท))) |
16 | 13, 14, 15 | sylc 65 |
. 2
โข
(((((๐ด โ
โ โง 0 โค ๐ด)
โง ๐ต โ โ)
โง ((๐ถ โ โ
โง 0 โค ๐ถ) โง ๐ท โ โ)) โง (๐ด โค ๐ต โง ๐ถ โค ๐ท)) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท)) |
17 | 16 | ex 414 |
1
โข ((((๐ด โ โ โง 0 โค
๐ด) โง ๐ต โ โ) โง ((๐ถ โ โ โง 0 โค ๐ถ) โง ๐ท โ โ)) โ ((๐ด โค ๐ต โง ๐ถ โค ๐ท) โ (๐ด ยท ๐ถ) โค (๐ต ยท ๐ท))) |