Description: Commuted version of ax-1rid without ax-mulcom . (Contributed by SN, 5-Feb-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | remulid2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne | |
|
2 | ax-rrecex | |
|
3 | simpll | |
|
4 | 3 | recnd | |
5 | simprl | |
|
6 | 5 | recnd | |
7 | 4 6 4 | mulassd | |
8 | simprr | |
|
9 | 8 | oveq1d | |
10 | 3 5 8 | remulinvcom | |
11 | 10 | oveq2d | |
12 | ax-1rid | |
|
13 | 3 12 | syl | |
14 | 11 13 | eqtrd | |
15 | 7 9 14 | 3eqtr3d | |
16 | 2 15 | rexlimddv | |
17 | 16 | ex | |
18 | 1 17 | syl5bir | |
19 | 1re | |
|
20 | remul01 | |
|
21 | 19 20 | mp1i | |
22 | oveq2 | |
|
23 | id | |
|
24 | 21 22 23 | 3eqtr4d | |
25 | 18 24 | pm2.61d2 | |