QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  df-a3 Unicode version
Definition df-a3 55
Description: Defined conjunction.
Assertion
Ref Expression
df-a3 (a ^3 b) = (a' u3 b')'
Detailed syntax breakdown of Definition df-a3
StepHypRef Expression
1 wva . . 3 term a
2 wvb . . 3 term b
31, 2wan3 26 . 2 term (a ^3 b)
41wn 4 . . . 4 term a'
52wn 4 . . . 4 term b'
64, 5wo3 25 . . 3 term (a' u3 b')
76wn 4 . 2 term (a' u3 b')'
83, 7wb 1 1 wff (a ^3 b) = (a' u3 b')'
Colors of variables: term
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator