Description: The predicate "is a monoid". (Contributed by FL, 2-Nov-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ismndo1.1 | |
|
Assertion | ismndo1 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ismndo1.1 | |
|
2 | 1 | ismndo | |
3 | 1 | smgrpmgm | |
4 | 3 | ad2antrl | |
5 | 1 | smgrpassOLD | |
6 | 5 | ad2antrl | |
7 | simprr | |
|
8 | 4 6 7 | 3jca | |
9 | 3simpa | |
|
10 | 1 | issmgrpOLD | |
11 | 9 10 | syl5ibr | |
12 | 11 | imp | |
13 | simpr3 | |
|
14 | 12 13 | jca | |
15 | 8 14 | impbida | |
16 | 2 15 | bitrd | |