Database
REAL AND COMPLEX NUMBERS
Derive the basic properties from the field axioms
Initial properties of the complex numbers
mul12i
Metamath Proof Explorer
Description: Commutative/associative law that swaps the first two factors in a triple
product. (Contributed by NM , 11-May-1999) (Proof shortened by Andrew
Salmon , 19-Nov-2011)
Ref
Expression
Hypotheses
mul.1
โข ๐ด โ โ
mul.2
โข ๐ต โ โ
mul.3
โข ๐ถ โ โ
Assertion
mul12i
โข ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) = ( ๐ต ยท ( ๐ด ยท ๐ถ ) )
Proof
Step
Hyp
Ref
Expression
1
mul.1
โข ๐ด โ โ
2
mul.2
โข ๐ต โ โ
3
mul.3
โข ๐ถ โ โ
4
mul12
โข ( ( ๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ ) โ ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) = ( ๐ต ยท ( ๐ด ยท ๐ถ ) ) )
5
1 2 3 4
mp3an
โข ( ๐ด ยท ( ๐ต ยท ๐ถ ) ) = ( ๐ต ยท ( ๐ด ยท ๐ถ ) )