Metamath Proof Explorer
Description: Alternate proof of 1t1e1 using a different set of axioms (add
ax-mulrcl , ax-i2m1 , ax-1ne0 , ax-rrecex and remove ax-resscn ,
ax-mulcom , ax-mulass , ax-distr ). (Contributed by Steven Nguyen, 20-Sep-2022) (Proof modification is discouraged.)
(New usage is discouraged.)
|
|
Ref |
Expression |
|
Assertion |
1t1e1ALT |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
1re |
|
2 |
|
ax-1rid |
|
3 |
1 2
|
ax-mp |
|