Definition df-c1 132

Description: Define 'commutes'. See df-c2 133 for the other direction.

Hypothesis

Ref	Expression
df-c1.1	a = ((a ^ b) v (a ^ b'))

Assertion

Ref	Expression
df-c1	a C b

Detailed syntax breakdown of Definition df-c1

Step	Hyp	Ref	Expression
1		wva	. 2 term a
2		wvb	. 2 term b
3	1, 2	wc 3	1 wff a C b

This definition is referenced by:  comm0 178  comm1 179  lecom 180  bctr 181  cbtr 182  comcom2 183  comcom 453  comcom5 458  comdr 466  com3i 467  df2c1 468  com2or 483  cmtr1com 493  i0cmtrcom 495  i3lem2 505  i1com 708

Copyright terms: Public domain