Step | Hyp | Ref
| Expression |
1 | | eldifn 4087 |
. . . . . . . 8
โข (๐ด โ (โ โ
โ) โ ยฌ ๐ด
โ โ) |
2 | 1 | 3ad2ant1 1133 |
. . . . . . 7
โข ((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โ ยฌ ๐ด
โ โ) |
3 | 2 | adantr 481 |
. . . . . 6
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ยฌ ๐ด โ โ) |
4 | | simpll1 1212 |
. . . . . . . . . . . 12
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ด โ (โ โ
โ)) |
5 | 4 | eldifad 3922 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ด โ โ) |
6 | | simp2r 1200 |
. . . . . . . . . . . . 13
โข ((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โ ๐ถ โ
โ) |
7 | 6 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ถ โ โ) |
8 | | qcn 12887 |
. . . . . . . . . . . 12
โข (๐ถ โ โ โ ๐ถ โ
โ) |
9 | 7, 8 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ถ โ โ) |
10 | | simp3r 1202 |
. . . . . . . . . . . . 13
โข ((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โ ๐ธ โ
โ) |
11 | 10 | ad2antrr 724 |
. . . . . . . . . . . 12
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ธ โ โ) |
12 | | qcn 12887 |
. . . . . . . . . . . 12
โข (๐ธ โ โ โ ๐ธ โ
โ) |
13 | 11, 12 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ธ โ โ) |
14 | 5, 9, 13 | subdid 11610 |
. . . . . . . . . 10
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ด ยท (๐ถ โ ๐ธ)) = ((๐ด ยท ๐ถ) โ (๐ด ยท ๐ธ))) |
15 | | qsubcl 12892 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โ โง ๐ธ โ โ) โ (๐ถ โ ๐ธ) โ โ) |
16 | 7, 11, 15 | syl2anc 584 |
. . . . . . . . . . . 12
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ถ โ ๐ธ) โ โ) |
17 | | qcn 12887 |
. . . . . . . . . . . 12
โข ((๐ถ โ ๐ธ) โ โ โ (๐ถ โ ๐ธ) โ โ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ถ โ ๐ธ) โ โ) |
19 | 18, 5 | mulcomd 11175 |
. . . . . . . . . 10
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ((๐ถ โ ๐ธ) ยท ๐ด) = (๐ด ยท (๐ถ โ ๐ธ))) |
20 | | simplr 767 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) |
21 | | simp2l 1199 |
. . . . . . . . . . . . . 14
โข ((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โ ๐ต โ
โ) |
22 | 21 | ad2antrr 724 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ต โ โ) |
23 | | qcn 12887 |
. . . . . . . . . . . . 13
โข (๐ต โ โ โ ๐ต โ
โ) |
24 | 22, 23 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ต โ โ) |
25 | 5, 9 | mulcld 11174 |
. . . . . . . . . . . 12
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ด ยท ๐ถ) โ โ) |
26 | | simp3l 1201 |
. . . . . . . . . . . . . 14
โข ((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โ ๐ท โ
โ) |
27 | 26 | ad2antrr 724 |
. . . . . . . . . . . . 13
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ท โ โ) |
28 | | qcn 12887 |
. . . . . . . . . . . . 13
โข (๐ท โ โ โ ๐ท โ
โ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . 12
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ท โ โ) |
30 | 5, 13 | mulcld 11174 |
. . . . . . . . . . . 12
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ด ยท ๐ธ) โ โ) |
31 | 24, 25, 29, 30 | addsubeq4d 11562 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ((๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ)) โ (๐ท โ ๐ต) = ((๐ด ยท ๐ถ) โ (๐ด ยท ๐ธ)))) |
32 | 20, 31 | mpbid 231 |
. . . . . . . . . 10
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ท โ ๐ต) = ((๐ด ยท ๐ถ) โ (๐ด ยท ๐ธ))) |
33 | 14, 19, 32 | 3eqtr4d 2786 |
. . . . . . . . 9
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ((๐ถ โ ๐ธ) ยท ๐ด) = (๐ท โ ๐ต)) |
34 | | qsubcl 12892 |
. . . . . . . . . . . 12
โข ((๐ท โ โ โง ๐ต โ โ) โ (๐ท โ ๐ต) โ โ) |
35 | 27, 22, 34 | syl2anc 584 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ท โ ๐ต) โ โ) |
36 | | qcn 12887 |
. . . . . . . . . . 11
โข ((๐ท โ ๐ต) โ โ โ (๐ท โ ๐ต) โ โ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . 10
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ท โ ๐ต) โ โ) |
38 | | simpr 485 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ยฌ ๐ถ = ๐ธ) |
39 | | subeq0 11426 |
. . . . . . . . . . . . 13
โข ((๐ถ โ โ โง ๐ธ โ โ) โ ((๐ถ โ ๐ธ) = 0 โ ๐ถ = ๐ธ)) |
40 | 39 | necon3abid 2980 |
. . . . . . . . . . . 12
โข ((๐ถ โ โ โง ๐ธ โ โ) โ ((๐ถ โ ๐ธ) โ 0 โ ยฌ ๐ถ = ๐ธ)) |
41 | 9, 13, 40 | syl2anc 584 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ((๐ถ โ ๐ธ) โ 0 โ ยฌ ๐ถ = ๐ธ)) |
42 | 38, 41 | mpbird 256 |
. . . . . . . . . 10
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (๐ถ โ ๐ธ) โ 0) |
43 | 37, 18, 5, 42 | divmuld 11952 |
. . . . . . . . 9
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ (((๐ท โ ๐ต) / (๐ถ โ ๐ธ)) = ๐ด โ ((๐ถ โ ๐ธ) ยท ๐ด) = (๐ท โ ๐ต))) |
44 | 33, 43 | mpbird 256 |
. . . . . . . 8
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ((๐ท โ ๐ต) / (๐ถ โ ๐ธ)) = ๐ด) |
45 | | qdivcl 12894 |
. . . . . . . . 9
โข (((๐ท โ ๐ต) โ โ โง (๐ถ โ ๐ธ) โ โ โง (๐ถ โ ๐ธ) โ 0) โ ((๐ท โ ๐ต) / (๐ถ โ ๐ธ)) โ โ) |
46 | 35, 16, 42, 45 | syl3anc 1371 |
. . . . . . . 8
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ((๐ท โ ๐ต) / (๐ถ โ ๐ธ)) โ โ) |
47 | 44, 46 | eqeltrrd 2839 |
. . . . . . 7
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ยฌ ๐ถ = ๐ธ) โ ๐ด โ โ) |
48 | 47 | ex 413 |
. . . . . 6
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ (ยฌ ๐ถ = ๐ธ โ ๐ด โ โ)) |
49 | 3, 48 | mt3d 148 |
. . . . 5
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ถ = ๐ธ) |
50 | | simpl2l 1226 |
. . . . . . . . 9
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ต โ โ) |
51 | 50, 23 | syl 17 |
. . . . . . . 8
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ต โ โ) |
52 | 51 | adantr 481 |
. . . . . . 7
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ ๐ต โ โ) |
53 | | simpl3l 1228 |
. . . . . . . . 9
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ท โ โ) |
54 | 53, 28 | syl 17 |
. . . . . . . 8
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ท โ โ) |
55 | 54 | adantr 481 |
. . . . . . 7
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ ๐ท โ โ) |
56 | | simpl1 1191 |
. . . . . . . . . 10
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ด โ (โ โ
โ)) |
57 | 56 | eldifad 3922 |
. . . . . . . . 9
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ด โ โ) |
58 | | simpl3r 1229 |
. . . . . . . . . 10
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ธ โ โ) |
59 | 58, 12 | syl 17 |
. . . . . . . . 9
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ ๐ธ โ โ) |
60 | 57, 59 | mulcld 11174 |
. . . . . . . 8
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ (๐ด ยท ๐ธ) โ โ) |
61 | 60 | adantr 481 |
. . . . . . 7
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ (๐ด ยท ๐ธ) โ โ) |
62 | | simpr 485 |
. . . . . . . . . . 11
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ ๐ถ = ๐ธ) |
63 | 62 | eqcomd 2742 |
. . . . . . . . . 10
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ ๐ธ = ๐ถ) |
64 | 63 | oveq2d 7372 |
. . . . . . . . 9
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ (๐ด ยท ๐ธ) = (๐ด ยท ๐ถ)) |
65 | 64 | oveq2d 7372 |
. . . . . . . 8
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ (๐ต + (๐ด ยท ๐ธ)) = (๐ต + (๐ด ยท ๐ถ))) |
66 | | simplr 767 |
. . . . . . . 8
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) |
67 | 65, 66 | eqtrd 2776 |
. . . . . . 7
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ (๐ต + (๐ด ยท ๐ธ)) = (๐ท + (๐ด ยท ๐ธ))) |
68 | 52, 55, 61, 67 | addcan2ad 11360 |
. . . . . 6
โข ((((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โง ๐ถ = ๐ธ) โ ๐ต = ๐ท) |
69 | 68 | ex 413 |
. . . . 5
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ (๐ถ = ๐ธ โ ๐ต = ๐ท)) |
70 | 49, 69 | jcai 517 |
. . . 4
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ (๐ถ = ๐ธ โง ๐ต = ๐ท)) |
71 | 70 | ancomd 462 |
. . 3
โข (((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โง (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) โ (๐ต = ๐ท โง ๐ถ = ๐ธ)) |
72 | 71 | ex 413 |
. 2
โข ((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โ ((๐ต +
(๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ)) โ (๐ต = ๐ท โง ๐ถ = ๐ธ))) |
73 | | id 22 |
. . 3
โข (๐ต = ๐ท โ ๐ต = ๐ท) |
74 | | oveq2 7364 |
. . 3
โข (๐ถ = ๐ธ โ (๐ด ยท ๐ถ) = (๐ด ยท ๐ธ)) |
75 | 73, 74 | oveqan12d 7375 |
. 2
โข ((๐ต = ๐ท โง ๐ถ = ๐ธ) โ (๐ต + (๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ))) |
76 | 72, 75 | impbid1 224 |
1
โข ((๐ด โ (โ โ
โ) โง (๐ต โ
โ โง ๐ถ โ
โ) โง (๐ท โ
โ โง ๐ธ โ
โ)) โ ((๐ต +
(๐ด ยท ๐ถ)) = (๐ท + (๐ด ยท ๐ธ)) โ (๐ต = ๐ท โง ๐ถ = ๐ธ))) |