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

Theorem u1lemonb 635
 Description: Lemma for Sasaki implication study.
Assertion
Ref Expression
u1lemonb ((a1 b) ∪ b ) = 1

Proof of Theorem u1lemonb
StepHypRef Expression
1 df-i1 44 . . 3 (a1 b) = (a ∪ (ab))
21ax-r5 38 . 2 ((a1 b) ∪ b ) = ((a ∪ (ab)) ∪ b )
3 or32 82 . . 3 ((a ∪ (ab)) ∪ b ) = ((ab ) ∪ (ab))
4 df-a 40 . . . . 5 (ab) = (ab )
54lor 70 . . . 4 ((ab ) ∪ (ab)) = ((ab ) ∪ (ab ) )
6 df-t 41 . . . . 5 1 = ((ab ) ∪ (ab ) )
76ax-r1 35 . . . 4 ((ab ) ∪ (ab ) ) = 1
85, 7ax-r2 36 . . 3 ((ab ) ∪ (ab)) = 1
93, 8ax-r2 36 . 2 ((a ∪ (ab)) ∪ b ) = 1
102, 9ax-r2 36 1 ((a1 b) ∪ b ) = 1
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →1 wi1 12 This theorem was proved from axioms:  ax-a2 31  ax-a3 32  ax-r1 35  ax-r2 36  ax-r5 38 This theorem depends on definitions:  df-a 40  df-t 41  df-i1 44 This theorem is referenced by:  u1lemnab  650  u3lem14a  791
 Copyright terms: Public domain W3C validator