Theorem assintopass

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

	Ref	Expression
Assertion	assintopass	Could not format assertion : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		id	Could not format ( .o. e. ( assIntOp ` M ) -> .o. e. ( assIntOp ` M ) ) : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> .o. e. ( assIntOp ` M ) ) with typecode |-
2		elfvex	Could not format ( .o. e. ( assIntOp ` M ) -> M e. _V ) : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> M e. _V ) with typecode |-
3		assintopasslaw	Could not format ( .o. e. ( assIntOp ` M ) -> .o. assLaw M ) : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> .o. assLaw M ) with typecode |-
4		isasslaw	Could not format ( ( .o. e. ( assIntOp ` M ) /\ M e. _V ) -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( ( .o. e. ( assIntOp ` M ) /\ M e. _V ) -> ( .o. assLaw M <-> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
5	3 4	syl5ibcom	Could not format ( .o. e. ( assIntOp ` M ) -> ( ( .o. e. ( assIntOp ` M ) /\ M e. _V ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> ( ( .o. e. ( assIntOp ` M ) /\ M e. _V ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) ) with typecode |-
6	1 2 5	mp2and	Could not format ( .o. e. ( assIntOp ` M ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) : No typesetting found for |- ( .o. e. ( assIntOp ` M ) -> A. x e. M A. y e. M A. z e. M ( ( x .o. y ) .o. z ) = ( x .o. ( y .o. z ) ) ) with typecode |-