Step |
Hyp |
Ref |
Expression |
1 |
|
decaddcom.a |
|
2 |
|
decaddcom.b |
|
3 |
|
decaddcom.c |
|
4 |
|
eqid |
Could not format ; A B = ; A B : No typesetting found for |- ; A B = ; A B with typecode |- |
5 |
|
eqid |
|
6 |
1 2 3 4 5
|
decaddi |
Could not format ( ; A B + C ) = ; A ( B + C ) : No typesetting found for |- ( ; A B + C ) = ; A ( B + C ) with typecode |- |
7 |
|
eqid |
Could not format ; A C = ; A C : No typesetting found for |- ; A C = ; A C with typecode |- |
8 |
3
|
nn0cni |
|
9 |
2
|
nn0cni |
|
10 |
8 9
|
addcomi |
|
11 |
1 3 2 7 10
|
decaddi |
Could not format ( ; A C + B ) = ; A ( B + C ) : No typesetting found for |- ( ; A C + B ) = ; A ( B + C ) with typecode |- |
12 |
6 11
|
eqtr4i |
Could not format ( ; A B + C ) = ( ; A C + B ) : No typesetting found for |- ( ; A B + C ) = ( ; A C + B ) with typecode |- |