Theorem cmtrcom 182

Description: Commutative law for commutator.

Assertion

Ref	Expression
cmtrcom	C (a, b) = C (b, a)

Proof of Theorem cmtrcom

Step	Hyp	Ref	Expression
1		ancom 68	. . . . 5 (a ^ b) = (b ^ a)
2		ancom 68	. . . . 5 (a ^ b_|_) = (b_|_ ^ a)
3	1, 2	2or 67	. . . 4 ((a ^ b) v (a ^ b_|_)) = ((b ^ a) v (b_|_ ^ a))
4		ancom 68	. . . . 5 (a_|_ ^ b) = (b ^ a_|_)
5		ancom 68	. . . . 5 (a_|_ ^ b_|_) = (b_|_ ^ a_|_)
6	4, 5	2or 67	. . . 4 ((a_|_ ^ b) v (a_|_ ^ b_|_)) = ((b ^ a_|_) v (b_|_ ^ a_|_))
7	3, 6	2or 67	. . 3 (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (a_|_ ^ b_|_))) = (((b ^ a) v (b_|_ ^ a)) v ((b ^ a_|_) v (b_|_ ^ a_|_)))
8		or4 77	. . 3 (((b ^ a) v (b_|_ ^ a)) v ((b ^ a_|_) v (b_|_ ^ a_|_))) = (((b ^ a) v (b ^ a_|_)) v ((b_|_ ^ a) v (b_|_ ^ a_|_)))
9	7, 8	ax-r2 35	. 2 (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (a_|_ ^ b_|_))) = (((b ^ a) v (b ^ a_|_)) v ((b_|_ ^ a) v (b_|_ ^ a_|_)))
10		df-cmtr 126	. 2 C (a, b) = (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
11		df-cmtr 126	. 2 C (b, a) = (((b ^ a) v (b ^ a_|_)) v ((b_|_ ^ a) v (b_|_ ^ a_|_)))
12	9, 10, 11	3tr1 60	1 C (a, b) = C (b, a)

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7   C wcmtr 28

This theorem is referenced by:  wdf-c1 365  wcomcom 396  3vded3 801

This theorem was proved from axioms:  ax-a2 30  ax-a3 31  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-a 39  df-cmtr 126

metamath.org