Metamath Proof Explorer

Theorem hvadd32

Description: Commutative/associative law. (Contributed by NM, 16-Oct-1999) (New usage is discouraged.)

Ref Expression
Assertion hvadd32 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC=A+ℎC+ℎB

Proof

Step Hyp Ref Expression
1 ax-hvcom ⊢B∈ℋ∧C∈ℋ→B+ℎC=C+ℎB
2 1 oveq2d ⊢B∈ℋ∧C∈ℋ→A+ℎB+ℎC=A+ℎC+ℎB
3 2 3adant1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC=A+ℎC+ℎB
4 ax-hvass ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC=A+ℎB+ℎC
5 ax-hvass ⊢A∈ℋ∧C∈ℋ∧B∈ℋ→A+ℎC+ℎB=A+ℎC+ℎB
6 5 3com23 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎC+ℎB=A+ℎC+ℎB
7 3 4 6 3eqtr4d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC=A+ℎC+ℎB