QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-c1 GIF version

Definition df-c1 132
Description: Define "commutes". See df-c2 133 for the other direction. (Contributed by NM, 27-Aug-1997.)
Hypothesis
Ref Expression
df-c1.1 a = ((ab) ∪ (ab ))
Assertion
Ref Expression
df-c1 a C b

Detailed syntax breakdown of Definition df-c1
StepHypRef Expression
1 wva . 2 term  a
2 wvb . 2 term  b
31, 2wc 3 1 wff  a C b
Colors of variables: term
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 W3C validator