Definition df-c1 126

Description: Define 'commutes'. See df-c2 127 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 172  comm1 173  lecom 174  bctr 175  cbtr 176  comcom2 177  comcom 439  comcom5 444  comdr 452  com3i 453  df2c1 454  com2or 469  cmtr1com 479  i0cmtrcom 481  i3lem2 491  i1com 694

Copyright terms: Public domain