Metamath Proof Explorer


Theorem mul4d

Description: Rearrangement of 4 factors. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses muld.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
addcomd.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
addcand.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
mul4d.4 โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„‚ )
Assertion mul4d ( ๐œ‘ โ†’ ( ( ๐ด ยท ๐ต ) ยท ( ๐ถ ยท ๐ท ) ) = ( ( ๐ด ยท ๐ถ ) ยท ( ๐ต ยท ๐ท ) ) )

Proof

Step Hyp Ref Expression
1 muld.1 โŠข ( ๐œ‘ โ†’ ๐ด โˆˆ โ„‚ )
2 addcomd.2 โŠข ( ๐œ‘ โ†’ ๐ต โˆˆ โ„‚ )
3 addcand.3 โŠข ( ๐œ‘ โ†’ ๐ถ โˆˆ โ„‚ )
4 mul4d.4 โŠข ( ๐œ‘ โ†’ ๐ท โˆˆ โ„‚ )
5 mul4 โŠข ( ( ( ๐ด โˆˆ โ„‚ โˆง ๐ต โˆˆ โ„‚ ) โˆง ( ๐ถ โˆˆ โ„‚ โˆง ๐ท โˆˆ โ„‚ ) ) โ†’ ( ( ๐ด ยท ๐ต ) ยท ( ๐ถ ยท ๐ท ) ) = ( ( ๐ด ยท ๐ถ ) ยท ( ๐ต ยท ๐ท ) ) )
6 1 2 3 4 5 syl22anc โŠข ( ๐œ‘ โ†’ ( ( ๐ด ยท ๐ต ) ยท ( ๐ถ ยท ๐ท ) ) = ( ( ๐ด ยท ๐ถ ) ยท ( ๐ต ยท ๐ท ) ) )