Step |
Hyp |
Ref |
Expression |
1 |
|
mgm2nsgrp.s |
|
2 |
|
mgm2nsgrp.b |
|
3 |
|
sgrp2nmnd.o |
|
4 |
|
sgrp2nmnd.p |
Could not format .o. = ( +g ` M ) : No typesetting found for |- .o. = ( +g ` M ) with typecode |- |
5 |
4 3
|
eqtri |
Could not format .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) : No typesetting found for |- .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) with typecode |- |
6 |
5
|
a1i |
Could not format ( ( A e. S /\ C e. S ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) ) : No typesetting found for |- ( ( A e. S /\ C e. S ) -> .o. = ( x e. S , y e. S |-> if ( x = A , A , B ) ) ) with typecode |- |
7 |
|
iftrue |
|
8 |
7
|
ad2antrl |
|
9 |
|
simpl |
|
10 |
|
simpr |
|
11 |
6 8 9 10 9
|
ovmpod |
Could not format ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A ) : No typesetting found for |- ( ( A e. S /\ C e. S ) -> ( A .o. C ) = A ) with typecode |- |