Step | Hyp | Ref
| Expression |
1 | | simpl 109 |
. . . . . . 7
โข ((๐ด = โ
โง ๐ต = โ
) โ ๐ด = โ
) |
2 | | simpl 109 |
. . . . . . 7
โข ((๐ด = โ
โง โ
โ
๐ต) โ ๐ด = โ
) |
3 | 1, 2 | jaoi 716 |
. . . . . 6
โข (((๐ด = โ
โง ๐ต = โ
) โจ (๐ด = โ
โง โ
โ
๐ต)) โ ๐ด = โ
) |
4 | 3 | orcd 733 |
. . . . 5
โข (((๐ด = โ
โง ๐ต = โ
) โจ (๐ด = โ
โง โ
โ
๐ต)) โ (๐ด = โ
โจ ๐ต = โ
)) |
5 | 4 | a1i 9 |
. . . 4
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โ (((๐ด = โ
โง ๐ต = โ
) โจ (๐ด = โ
โง โ
โ
๐ต)) โ (๐ด = โ
โจ ๐ต = โ
))) |
6 | | simpr 110 |
. . . . . . 7
โข ((โ
โ ๐ด โง ๐ต = โ
) โ ๐ต = โ
) |
7 | 6 | olcd 734 |
. . . . . 6
โข ((โ
โ ๐ด โง ๐ต = โ
) โ (๐ด = โ
โจ ๐ต = โ
)) |
8 | 7 | a1i 9 |
. . . . 5
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โ ((โ
โ ๐ด โง ๐ต = โ
) โ (๐ด = โ
โจ ๐ต = โ
))) |
9 | | simplr 528 |
. . . . . . 7
โข ((((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โง (โ
โ ๐ด โง โ
โ ๐ต)) โ (๐ด ยทo ๐ต) = โ
) |
10 | | nnmordi 6516 |
. . . . . . . . . . . . 13
โข (((๐ต โ ฯ โง ๐ด โ ฯ) โง โ
โ ๐ด) โ (โ
โ ๐ต โ (๐ด ยทo โ
)
โ (๐ด
ยทo ๐ต))) |
11 | 10 | expimpd 363 |
. . . . . . . . . . . 12
โข ((๐ต โ ฯ โง ๐ด โ ฯ) โ
((โ
โ ๐ด โง
โ
โ ๐ต) โ
(๐ด ยทo
โ
) โ (๐ด
ยทo ๐ต))) |
12 | 11 | ancoms 268 |
. . . . . . . . . . 11
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ
((โ
โ ๐ด โง
โ
โ ๐ต) โ
(๐ด ยทo
โ
) โ (๐ด
ยทo ๐ต))) |
13 | | nnm0 6475 |
. . . . . . . . . . . . 13
โข (๐ด โ ฯ โ (๐ด ยทo โ
) =
โ
) |
14 | 13 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (๐ด ยทo โ
) =
โ
) |
15 | 14 | eleq1d 2246 |
. . . . . . . . . . 11
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo โ
)
โ (๐ด
ยทo ๐ต)
โ โ
โ (๐ด
ยทo ๐ต))) |
16 | 12, 15 | sylibd 149 |
. . . . . . . . . 10
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ
((โ
โ ๐ด โง
โ
โ ๐ต) โ
โ
โ (๐ด
ยทo ๐ต))) |
17 | 16 | adantr 276 |
. . . . . . . . 9
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โ ((โ
โ ๐ด โง โ
โ ๐ต) โ โ
โ (๐ด
ยทo ๐ต))) |
18 | 17 | imp 124 |
. . . . . . . 8
โข ((((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โง (โ
โ ๐ด โง โ
โ ๐ต)) โ โ
โ (๐ด
ยทo ๐ต)) |
19 | | n0i 3428 |
. . . . . . . 8
โข (โ
โ (๐ด
ยทo ๐ต)
โ ยฌ (๐ด
ยทo ๐ต) =
โ
) |
20 | 18, 19 | syl 14 |
. . . . . . 7
โข ((((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โง (โ
โ ๐ด โง โ
โ ๐ต)) โ ยฌ
(๐ด ยทo
๐ต) =
โ
) |
21 | 9, 20 | pm2.21dd 620 |
. . . . . 6
โข ((((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โง (โ
โ ๐ด โง โ
โ ๐ต)) โ (๐ด = โ
โจ ๐ต = โ
)) |
22 | 21 | ex 115 |
. . . . 5
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โ ((โ
โ ๐ด โง โ
โ ๐ต) โ (๐ด = โ
โจ ๐ต = โ
))) |
23 | 8, 22 | jaod 717 |
. . . 4
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โ (((โ
โ ๐ด โง ๐ต = โ
) โจ (โ
โ
๐ด โง โ
โ
๐ต)) โ (๐ด = โ
โจ ๐ต = โ
))) |
24 | | 0elnn 4618 |
. . . . . . 7
โข (๐ด โ ฯ โ (๐ด = โ
โจ โ
โ
๐ด)) |
25 | | 0elnn 4618 |
. . . . . . 7
โข (๐ต โ ฯ โ (๐ต = โ
โจ โ
โ
๐ต)) |
26 | 24, 25 | anim12i 338 |
. . . . . 6
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด = โ
โจ โ
โ
๐ด) โง (๐ต = โ
โจ โ
โ ๐ต))) |
27 | | anddi 821 |
. . . . . 6
โข (((๐ด = โ
โจ โ
โ
๐ด) โง (๐ต = โ
โจ โ
โ ๐ต)) โ (((๐ด = โ
โง ๐ต = โ
) โจ (๐ด = โ
โง โ
โ ๐ต)) โจ ((โ
โ ๐ด โง ๐ต = โ
) โจ (โ
โ ๐ด โง โ
โ ๐ต)))) |
28 | 26, 27 | sylib 122 |
. . . . 5
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (((๐ด = โ
โง ๐ต = โ
) โจ (๐ด = โ
โง โ
โ
๐ต)) โจ ((โ
โ
๐ด โง ๐ต = โ
) โจ (โ
โ ๐ด โง โ
โ ๐ต)))) |
29 | 28 | adantr 276 |
. . . 4
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โ (((๐ด = โ
โง ๐ต = โ
) โจ (๐ด = โ
โง โ
โ
๐ต)) โจ ((โ
โ
๐ด โง ๐ต = โ
) โจ (โ
โ ๐ด โง โ
โ ๐ต)))) |
30 | 5, 23, 29 | mpjaod 718 |
. . 3
โข (((๐ด โ ฯ โง ๐ต โ ฯ) โง (๐ด ยทo ๐ต) = โ
) โ (๐ด = โ
โจ ๐ต = โ
)) |
31 | 30 | ex 115 |
. 2
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) = โ
โ (๐ด = โ
โจ ๐ต = โ
))) |
32 | | oveq1 5881 |
. . . . . 6
โข (๐ด = โ
โ (๐ด ยทo ๐ต) = (โ
ยทo ๐ต)) |
33 | | nnm0r 6479 |
. . . . . 6
โข (๐ต โ ฯ โ (โ
ยทo ๐ต) =
โ
) |
34 | 32, 33 | sylan9eqr 2232 |
. . . . 5
โข ((๐ต โ ฯ โง ๐ด = โ
) โ (๐ด ยทo ๐ต) = โ
) |
35 | 34 | ex 115 |
. . . 4
โข (๐ต โ ฯ โ (๐ด = โ
โ (๐ด ยทo ๐ต) = โ
)) |
36 | 35 | adantl 277 |
. . 3
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (๐ด = โ
โ (๐ด ยทo ๐ต) = โ
)) |
37 | | oveq2 5882 |
. . . . . 6
โข (๐ต = โ
โ (๐ด ยทo ๐ต) = (๐ด ยทo
โ
)) |
38 | 37, 13 | sylan9eqr 2232 |
. . . . 5
โข ((๐ด โ ฯ โง ๐ต = โ
) โ (๐ด ยทo ๐ต) = โ
) |
39 | 38 | ex 115 |
. . . 4
โข (๐ด โ ฯ โ (๐ต = โ
โ (๐ด ยทo ๐ต) = โ
)) |
40 | 39 | adantr 276 |
. . 3
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ (๐ต = โ
โ (๐ด ยทo ๐ต) = โ
)) |
41 | 36, 40 | jaod 717 |
. 2
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด = โ
โจ ๐ต = โ
) โ (๐ด ยทo ๐ต) = โ
)) |
42 | 31, 41 | impbid 129 |
1
โข ((๐ด โ ฯ โง ๐ต โ ฯ) โ ((๐ด ยทo ๐ต) = โ
โ (๐ด = โ
โจ ๐ต = โ
))) |