Metamath Proof Explorer


Theorem mullid

Description: Identity law for multiplication. See mulrid for commuted version. (Contributed by NM, 8-Oct-1999)

Ref Expression
Assertion mullid A 1 A = A

Proof

Step Hyp Ref Expression
1 ax-1cn 1
2 mulcom 1 A 1 A = A 1
3 1 2 mpan A 1 A = A 1
4 mulrid A A 1 = A
5 3 4 eqtrd A 1 A = A