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