Theorem smgrpismgmOLD

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

	Ref	Expression
Assertion	smgrpismgmOLD	$$⊢G\in \mathrm{SemiGrp}\to G\in \mathrm{Magma}$$

Proof

Step	Hyp	Ref	Expression
1		elin	$$⊢G\in \left(\mathrm{Magma}\cap \mathrm{Ass}\right)\leftrightarrow \left(G\in \mathrm{Magma}\wedge G\in \mathrm{Ass}\right)$$
2	1	simplbi	$$⊢G\in \left(\mathrm{Magma}\cap \mathrm{Ass}\right)\to G\in \mathrm{Magma}$$
3		df-sgrOLD	$$⊢\mathrm{SemiGrp}=\mathrm{Magma}\cap \mathrm{Ass}$$
4	2 3	eleq2s	$$⊢G\in \mathrm{SemiGrp}\to G\in \mathrm{Magma}$$