Definition df-c2 133

Description: Define 'commutes'. See df-c1 132 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 181  cbtr 182  comcom2 183  wwcomd 214  wcom0 407  wcom1 408  comcom 453  comd 456  comcom5 458  com2or 483  comcmtr1 494  comi1 709

Copyright terms: Public domain