Metamath Proof Explorer

Theorem hvadd12

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

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

Proof

Step Hyp Ref Expression
1 ax-hvcom ⊢A∈ℋ∧B∈ℋ→A+ℎB=B+ℎA
2 1 oveq1d ⊢A∈ℋ∧B∈ℋ→A+ℎB+ℎC=B+ℎA+ℎC
3 2 3adant3 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC=B+ℎA+ℎC
4 ax-hvass ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC=A+ℎB+ℎC
5 ax-hvass ⊢B∈ℋ∧A∈ℋ∧C∈ℋ→B+ℎA+ℎC=B+ℎA+ℎC
6 5 3com12 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→B+ℎA+ℎC=B+ℎA+ℎC
7 3 4 6 3eqtr3d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎB+ℎC=B+ℎA+ℎC