Metamath Proof Explorer

Theorem smgrpassOLD

Description: Obsolete version of sgrpass as of 3-Feb-2020. A semigroup is associative. (Contributed by FL, 2-Nov-2009) (New usage is discouraged.) (Proof modification is discouraged.)

		Ref	Expression
	Hypothesis	smgrpassOLD.1	$⊢ X = dom dom G$
	Assertion	smgrpassOLD	$⊢ G \in SemiGrp \to \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)$

Proof

Step	Hyp	Ref	Expression
1		smgrpassOLD.1	$⊢ X = dom dom G$
2	1	issmgrpOLD	$⊢ G \in SemiGrp \to (G \in SemiGrp \leftrightarrow (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)))$
3		simpr	$⊢ (G : X \times X ⟶ X \land \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)) \to \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)$
4	2 3	syl6bi	$⊢ G \in SemiGrp \to (G \in SemiGrp \to \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z))$
5	4	pm2.43i	$⊢ G \in SemiGrp \to \forall x \in X \forall y \in X \forall z \in X (x G y) G z = x G (y G z)$