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

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

Detailed syntax breakdown of Definition df-c2
StepHypRef Expression
1 wva . 2 term  a
2 wvb . . . 4 term  b
31, 2wa 7 . . 3 term  (ab)
42wn 4 . . . 4 term  b
51, 4wa 7 . . 3 term  (ab )
63, 5wo 6 . 2 term  ((ab) ∪ (ab ))
71, 6wb 1 1 wff  a = ((ab) ∪ (ab ))
Colors of variables: term
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 W3C validator