hvadd32

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

		Ref	Expression
	Assertion	hvadd32	$⊢ (A \in ℋ \land B \in ℋ \land C \in ℋ) \to (A +_{ℎ} B) +_{ℎ} C = (A +_{ℎ} C) +_{ℎ} B$

Step	Hyp	Ref	Expression
1		ax-hvcom	$⊢ (B \in ℋ \land C \in ℋ) \to B +_{ℎ} C = C +_{ℎ} B$
2	1	oveq2d	$⊢ (B \in ℋ \land C \in ℋ) \to A +_{ℎ} (B +_{ℎ} C) = A +_{ℎ} (C +_{ℎ} B)$
3	2	3adant1	$⊢ (A \in ℋ \land B \in ℋ \land C \in ℋ) \to A +_{ℎ} (B +_{ℎ} C) = A +_{ℎ} (C +_{ℎ} B)$
4		ax-hvass	$⊢ (A \in ℋ \land B \in ℋ \land C \in ℋ) \to (A +_{ℎ} B) +_{ℎ} C = A +_{ℎ} (B +_{ℎ} C)$
5		ax-hvass	$⊢ (A \in ℋ \land C \in ℋ \land B \in ℋ) \to (A +_{ℎ} C) +_{ℎ} B = A +_{ℎ} (C +_{ℎ} B)$
6	5	3com23	$⊢ (A \in ℋ \land B \in ℋ \land C \in ℋ) \to (A +_{ℎ} C) +_{ℎ} B = A +_{ℎ} (C +_{ℎ} B)$
7	3 4 6	3eqtr4d	$⊢ (A \in ℋ \land B \in ℋ \land C \in ℋ) \to (A +_{ℎ} B) +_{ℎ} C = (A +_{ℎ} C) +_{ℎ} B$

Metamath Proof Explorer