Step |
Hyp |
Ref |
Expression |
1 |
|
hoaddcom |
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( S +op T ) = ( T +op S ) ) |
2 |
1
|
oveq1d |
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( T +op S ) -op U ) ) |
3 |
2
|
3adant3 |
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( T +op S ) -op U ) ) |
4 |
|
hoaddsubass |
|- ( ( T : ~H --> ~H /\ S : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( T +op S ) -op U ) = ( T +op ( S -op U ) ) ) |
5 |
4
|
3com12 |
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( T +op S ) -op U ) = ( T +op ( S -op U ) ) ) |
6 |
|
hosubcl |
|- ( ( S : ~H --> ~H /\ U : ~H --> ~H ) -> ( S -op U ) : ~H --> ~H ) |
7 |
|
hoaddcom |
|- ( ( T : ~H --> ~H /\ ( S -op U ) : ~H --> ~H ) -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) |
8 |
7
|
ex |
|- ( T : ~H --> ~H -> ( ( S -op U ) : ~H --> ~H -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) ) |
9 |
6 8
|
syl5 |
|- ( T : ~H --> ~H -> ( ( S : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) ) |
10 |
9
|
expd |
|- ( T : ~H --> ~H -> ( S : ~H --> ~H -> ( U : ~H --> ~H -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) ) ) |
11 |
10
|
com12 |
|- ( S : ~H --> ~H -> ( T : ~H --> ~H -> ( U : ~H --> ~H -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) ) ) |
12 |
11
|
3imp |
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( T +op ( S -op U ) ) = ( ( S -op U ) +op T ) ) |
13 |
3 5 12
|
3eqtrd |
|- ( ( S : ~H --> ~H /\ T : ~H --> ~H /\ U : ~H --> ~H ) -> ( ( S +op T ) -op U ) = ( ( S -op U ) +op T ) ) |