QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-c2 Unicode version
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
StepHypRef Expression
1 wva . 2 term a
2 wvb . . . 4 term b
31, 2wa 7 . . 3 term (a ^ b)
42wn 4 . . . 4 term b'
51, 4wa 7 . . 3 term (a ^ b')
63, 5wo 6 . 2 term ((a ^ b) v (a ^ b'))
71, 6wb 1 1 wff a = ((a ^ b) v (a ^ b'))
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