Metamath Proof Explorer


Theorem assintopasslaw

Description: The associative low holds for a associative (closed internal binary) operation for a set. (Contributed by FL, 2-Nov-2009) (Revised by AV, 20-Jan-2020)

Ref Expression
Assertion assintopasslaw ( ∈ ( assIntOp ‘ 𝑀 ) → assLaw 𝑀 )

Proof

Step Hyp Ref Expression
1 assintop ( ∈ ( assIntOp ‘ 𝑀 ) → ( : ( 𝑀 × 𝑀 ) ⟶ 𝑀 assLaw 𝑀 ) )
2 1 simprd ( ∈ ( assIntOp ‘ 𝑀 ) → assLaw 𝑀 )