Definition df-c2 125

Description: Define 'commutes'. See df-c1 124 for the other direction.

Hypothesis

Ref	Expression
df-c2.1	a C b

Assertion

Ref	Expression
df-c2	a = ((a ^ b) v (a ^ b_|_))

Detailed syntax breakdown of Definition df-c2

Step	Hyp	Ref	Expression
1		wva	. 2 term a
2		wvb	. . . 4 term b
3	1, 2	wa 7	. . 3 term (a ^ b)
4	2	wn 4	. . . 4 term b_|_
5	1, 4	wa 7	. . 3 term (a ^ b_|_)
6	3, 5	wo 6	. 2 term ((a ^ b) v (a ^ b_|_))
7	1, 6	wb 1	1 wff a = ((a ^ b) v (a ^ b_|_))

This definition is referenced by:  bctr 173  cbtr 174  comcom2 175  wwcomd 206  wcom0 389  wcom1 390  comcom 435  comd 438  comcom5 440  com2or 465  comcmtr1 476  comi1 691

metamath.org