Step | Hyp | Ref
| Expression |
1 | | mul32 11382 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ยท ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) ยท ๐ต)) |
2 | 1 | oveq1d 7426 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท)) |
3 | 2 | 3expa 1118 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท)) |
4 | 3 | adantrr 715 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท)) |
5 | | mulcl 11196 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) |
6 | | mulass 11200 |
. . . 4
โข (((๐ด ยท ๐ต) โ โ โง ๐ถ โ โ โง ๐ท โ โ) โ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท))) |
7 | 6 | 3expb 1120 |
. . 3
โข (((๐ด ยท ๐ต) โ โ โง (๐ถ โ โ โง ๐ท โ โ)) โ (((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท))) |
8 | 5, 7 | sylan 580 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ต) ยท ๐ถ) ยท ๐ท) = ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท))) |
9 | | mulcl 11196 |
. . . 4
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
10 | | mulass 11200 |
. . . . 5
โข (((๐ด ยท ๐ถ) โ โ โง ๐ต โ โ โง ๐ท โ โ) โ (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท))) |
11 | 10 | 3expb 1120 |
. . . 4
โข (((๐ด ยท ๐ถ) โ โ โง (๐ต โ โ โง ๐ท โ โ)) โ (((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท))) |
12 | 9, 11 | sylan 580 |
. . 3
โข (((๐ด โ โ โง ๐ถ โ โ) โง (๐ต โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท))) |
13 | 12 | an4s 658 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) ยท ๐ต) ยท ๐ท) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท))) |
14 | 4, 8, 13 | 3eqtr3d 2780 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ต) ยท (๐ถ ยท ๐ท)) = ((๐ด ยท ๐ถ) ยท (๐ต ยท ๐ท))) |