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
|- ( .o. e. ( assIntOp ` M ) -> .o. assLaw M )

Proof

Step Hyp Ref Expression
1 assintop
 |-  ( .o. e. ( assIntOp ` M ) -> ( .o. : ( M X. M ) --> M /\ .o. assLaw M ) )
2 1 simprd
 |-  ( .o. e. ( assIntOp ` M ) -> .o. assLaw M )