Step | Hyp | Ref
| Expression |
1 | | simp1 997 |
. . 3
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ ๐ด
โ N) |
2 | | simp2 998 |
. . 3
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ ๐ต
โ N) |
3 | | simp3 999 |
. . 3
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ ๐ถ
โ N) |
4 | | mulcompig 7326 |
. . . 4
โข ((๐ฅ โ N โง
๐ฆ โ N)
โ (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ)) |
5 | 4 | adantl 277 |
. . 3
โข (((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โง (๐ฅ
โ N โง ๐ฆ โ N)) โ (๐ฅ
ยทN ๐ฆ) = (๐ฆ ยทN ๐ฅ)) |
6 | | mulasspig 7327 |
. . . 4
โข ((๐ฅ โ N โง
๐ฆ โ N
โง ๐ง โ
N) โ ((๐ฅ
ยทN ๐ฆ) ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง))) |
7 | 6 | adantl 277 |
. . 3
โข (((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โง (๐ฅ
โ N โง ๐ฆ โ N โง ๐ง โ N)) โ
((๐ฅ
ยทN ๐ฆ) ยทN ๐ง) = (๐ฅ ยทN (๐ฆ
ยทN ๐ง))) |
8 | 1, 2, 3, 5, 7 | caov32d 6051 |
. 2
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ ((๐ด
ยทN ๐ต) ยทN ๐ถ) = ((๐ด ยทN ๐ถ)
ยทN ๐ต)) |
9 | | mulclpi 7323 |
. . . . . 6
โข ((๐ด โ N โง
๐ต โ N)
โ (๐ด
ยทN ๐ต) โ N) |
10 | | mulclpi 7323 |
. . . . . 6
โข ((๐ด โ N โง
๐ถ โ N)
โ (๐ด
ยทN ๐ถ) โ N) |
11 | 9, 10 | anim12i 338 |
. . . . 5
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ด โ
N โง ๐ถ
โ N)) โ ((๐ด ยทN ๐ต) โ N โง
(๐ด
ยทN ๐ถ) โ N)) |
12 | | simpr 110 |
. . . . . 6
โข (((๐ด โ N โง
๐ด โ N)
โง (๐ต โ
N โง ๐ถ
โ N)) โ (๐ต โ N โง ๐ถ โ
N)) |
13 | 12 | an4s 588 |
. . . . 5
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ด โ
N โง ๐ถ
โ N)) โ (๐ต โ N โง ๐ถ โ
N)) |
14 | 11, 13 | jca 306 |
. . . 4
โข (((๐ด โ N โง
๐ต โ N)
โง (๐ด โ
N โง ๐ถ
โ N)) โ (((๐ด ยทN ๐ต) โ N โง
(๐ด
ยทN ๐ถ) โ N) โง (๐ต โ N โง
๐ถ โ
N))) |
15 | 14 | 3impdi 1293 |
. . 3
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ (((๐ด ยทN ๐ต) โ N โง
(๐ด
ยทN ๐ถ) โ N) โง (๐ต โ N โง
๐ถ โ
N))) |
16 | | enqbreq 7351 |
. . 3
โข ((((๐ด
ยทN ๐ต) โ N โง (๐ด
ยทN ๐ถ) โ N) โง (๐ต โ N โง
๐ถ โ N))
โ (โจ(๐ด
ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ
~Q โจ๐ต, ๐ถโฉ โ ((๐ด ยทN ๐ต)
ยทN ๐ถ) = ((๐ด ยทN ๐ถ)
ยทN ๐ต))) |
17 | 15, 16 | syl 14 |
. 2
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ (โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ
~Q โจ๐ต, ๐ถโฉ โ ((๐ด ยทN ๐ต)
ยทN ๐ถ) = ((๐ด ยทN ๐ถ)
ยทN ๐ต))) |
18 | 8, 17 | mpbird 167 |
1
โข ((๐ด โ N โง
๐ต โ N
โง ๐ถ โ
N) โ โจ(๐ด ยทN ๐ต), (๐ด ยทN ๐ถ)โฉ
~Q โจ๐ต, ๐ถโฉ) |