Metamath Proof Explorer


Theorem mulid1d

Description: Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypothesis addcld.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
Assertion mulid1d ( ๐œ‘ โ†’ ( ๐ด ยท 1 ) = ๐ด )

Proof

Step Hyp Ref Expression
1 addcld.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
2 mulid1 โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ๐ด ยท 1 ) = ๐ด )
3 1 2 syl โŠข ( ๐œ‘ โ†’ ( ๐ด ยท 1 ) = ๐ด )