Step | Hyp | Ref
| Expression |
1 | | addcl 11191 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) |
2 | | adddi 11198 |
. . . 4
โข (((๐ด + ๐ต) โ โ โง ๐ถ โ โ โง ๐ท โ โ) โ ((๐ด + ๐ต) ยท (๐ถ + ๐ท)) = (((๐ด + ๐ต) ยท ๐ถ) + ((๐ด + ๐ต) ยท ๐ท))) |
3 | 2 | 3expb 1120 |
. . 3
โข (((๐ด + ๐ต) โ โ โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + ๐ต) ยท (๐ถ + ๐ท)) = (((๐ด + ๐ต) ยท ๐ถ) + ((๐ด + ๐ต) ยท ๐ท))) |
4 | 1, 3 | sylan 580 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + ๐ต) ยท (๐ถ + ๐ท)) = (((๐ด + ๐ต) ยท ๐ถ) + ((๐ด + ๐ต) ยท ๐ท))) |
5 | | adddir 11204 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด + ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ))) |
6 | 5 | 3expa 1118 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด + ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ))) |
7 | 6 | adantrr 715 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + ๐ต) ยท ๐ถ) = ((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ))) |
8 | | adddir 11204 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ท โ โ) โ ((๐ด + ๐ต) ยท ๐ท) = ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) |
9 | 8 | 3expa 1118 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ท โ โ) โ ((๐ด + ๐ต) ยท ๐ท) = ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) |
10 | 9 | adantrl 714 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + ๐ต) ยท ๐ท) = ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) |
11 | 7, 10 | oveq12d 7426 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด + ๐ต) ยท ๐ถ) + ((๐ด + ๐ต) ยท ๐ท)) = (((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ)) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)))) |
12 | | mulcl 11193 |
. . . . 5
โข ((๐ด โ โ โง ๐ถ โ โ) โ (๐ด ยท ๐ถ) โ โ) |
13 | 12 | ad2ant2r 745 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ด ยท ๐ถ) โ โ) |
14 | | mulcl 11193 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) โ โ) |
15 | 14 | ad2ant2lr 746 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ถ) โ โ) |
16 | | mulcl 11193 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ท โ โ) โ (๐ด ยท ๐ท) โ โ) |
17 | | mulcl 11193 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ท โ โ) โ (๐ต ยท ๐ท) โ โ) |
18 | | addcl 11191 |
. . . . . . 7
โข (((๐ด ยท ๐ท) โ โ โง (๐ต ยท ๐ท) โ โ) โ ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ โ) |
19 | 16, 17, 18 | syl2an 596 |
. . . . . 6
โข (((๐ด โ โ โง ๐ท โ โ) โง (๐ต โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ โ) |
20 | 19 | anandirs 677 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ท โ โ) โ ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ โ) |
21 | 20 | adantrl 714 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)) โ โ) |
22 | 13, 15, 21 | add32d 11440 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ)) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) = (((๐ด ยท ๐ถ) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) + (๐ต ยท ๐ถ))) |
23 | | mulcom 11195 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ท โ โ) โ (๐ต ยท ๐ท) = (๐ท ยท ๐ต)) |
24 | 23 | ad2ant2l 744 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ท) = (๐ท ยท ๐ต)) |
25 | 24 | oveq2d 7424 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) + (๐ด ยท ๐ท)) + (๐ต ยท ๐ท)) = (((๐ด ยท ๐ถ) + (๐ด ยท ๐ท)) + (๐ท ยท ๐ต))) |
26 | 16 | ad2ant2rl 747 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ด ยท ๐ท) โ โ) |
27 | 17 | ad2ant2l 744 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ท) โ โ) |
28 | 13, 26, 27 | addassd 11235 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) + (๐ด ยท ๐ท)) + (๐ต ยท ๐ท)) = ((๐ด ยท ๐ถ) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท)))) |
29 | | mulcl 11193 |
. . . . . . . 8
โข ((๐ท โ โ โง ๐ต โ โ) โ (๐ท ยท ๐ต) โ โ) |
30 | 29 | ancoms 459 |
. . . . . . 7
โข ((๐ต โ โ โง ๐ท โ โ) โ (๐ท ยท ๐ต) โ โ) |
31 | 30 | ad2ant2l 744 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ท ยท ๐ต) โ โ) |
32 | 13, 26, 31 | add32d 11440 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) + (๐ด ยท ๐ท)) + (๐ท ยท ๐ต)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + (๐ด ยท ๐ท))) |
33 | 25, 28, 32 | 3eqtr3d 2780 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ถ) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + (๐ด ยท ๐ท))) |
34 | | mulcom 11195 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ต ยท ๐ถ) = (๐ถ ยท ๐ต)) |
35 | 34 | ad2ant2lr 746 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ต ยท ๐ถ) = (๐ถ ยท ๐ต)) |
36 | 33, 35 | oveq12d 7426 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) + (๐ต ยท ๐ถ)) = ((((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + (๐ด ยท ๐ท)) + (๐ถ ยท ๐ต))) |
37 | | addcl 11191 |
. . . . . 6
โข (((๐ด ยท ๐ถ) โ โ โง (๐ท ยท ๐ต) โ โ) โ ((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ โ) |
38 | 12, 30, 37 | syl2an 596 |
. . . . 5
โข (((๐ด โ โ โง ๐ถ โ โ) โง (๐ต โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ โ) |
39 | 38 | an4s 658 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) โ โ) |
40 | | mulcl 11193 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ ยท ๐ต) โ โ) |
41 | 40 | ancoms 459 |
. . . . 5
โข ((๐ต โ โ โง ๐ถ โ โ) โ (๐ถ ยท ๐ต) โ โ) |
42 | 41 | ad2ant2lr 746 |
. . . 4
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ถ ยท ๐ต) โ โ) |
43 | 39, 26, 42 | addassd 11235 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
((((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + (๐ด ยท ๐ท)) + (๐ถ ยท ๐ต)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) |
44 | 22, 36, 43 | 3eqtrd 2776 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ยท ๐ถ) + (๐ต ยท ๐ถ)) + ((๐ด ยท ๐ท) + (๐ต ยท ๐ท))) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) |
45 | 4, 11, 44 | 3eqtrd 2776 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด + ๐ต) ยท (๐ถ + ๐ท)) = (((๐ด ยท ๐ถ) + (๐ท ยท ๐ต)) + ((๐ด ยท ๐ท) + (๐ถ ยท ๐ต)))) |