Step | Hyp | Ref
| Expression |
1 | | bi2.04 389 |
. . . 4
โข ((ยฌ
๐ = 0 โ ((๐ ยท ๐) = 0 โ ๐ = 0 )) โ ((๐ ยท ๐) = 0 โ (ยฌ ๐ = 0 โ ๐ = 0 ))) |
2 | | df-ne 2941 |
. . . . 5
โข (๐ โ 0 โ ยฌ ๐ = 0 ) |
3 | 2 | imbi1i 350 |
. . . 4
โข ((๐ โ 0 โ ((๐ ยท ๐) = 0 โ ๐ = 0 )) โ (ยฌ ๐ = 0 โ ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
4 | | df-or 847 |
. . . . 5
โข ((๐ = 0 โจ ๐ = 0 ) โ (ยฌ ๐ = 0 โ ๐ = 0 )) |
5 | 4 | imbi2i 336 |
. . . 4
โข (((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )) โ ((๐ ยท ๐) = 0 โ (ยฌ ๐ = 0 โ ๐ = 0 ))) |
6 | 1, 3, 5 | 3bitr4ri 304 |
. . 3
โข (((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )) โ (๐ โ 0 โ ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
7 | 6 | 2ralbii 3124 |
. 2
โข
(โ๐ โ
๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )) โ โ๐ โ ๐ต โ๐ โ ๐ต (๐ โ 0 โ ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
8 | | r19.21v 3173 |
. . 3
โข
(โ๐ โ
๐ต (๐ โ 0 โ ((๐ ยท ๐) = 0 โ ๐ = 0 )) โ (๐ โ 0 โ โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
9 | 8 | ralbii 3093 |
. 2
โข
(โ๐ โ
๐ต โ๐ โ ๐ต (๐ โ 0 โ ((๐ ยท ๐) = 0 โ ๐ = 0 )) โ โ๐ โ ๐ต (๐ โ 0 โ โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 ))) |
10 | | raldifsnb 4760 |
. 2
โข
(โ๐ โ
๐ต (๐ โ 0 โ โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 )) โ โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 )) |
11 | 7, 9, 10 | 3bitri 297 |
1
โข
(โ๐ โ
๐ต โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ (๐ = 0 โจ ๐ = 0 )) โ โ๐ โ (๐ต โ { 0 })โ๐ โ ๐ต ((๐ ยท ๐) = 0 โ ๐ = 0 )) |