hvadd12

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

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

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

Metamath Proof Explorer