Metamath Proof Explorer

Theorem mulid2

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

Ref Expression
Assertion mulid2 
|- ( A e. CC -> ( 1 x. A ) = A )

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 mulcom 
 |-  ( ( 1 e. CC /\ A e. CC ) -> ( 1 x. A ) = ( A x. 1 ) )
3 1 2 mpan 
 |-  ( A e. CC -> ( 1 x. A ) = ( A x. 1 ) )
4 mulid1 
 |-  ( A e. CC -> ( A x. 1 ) = A )
5 3 4 eqtrd 
 |-  ( A e. CC -> ( 1 x. A ) = A )