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

Theorem u2lem7 773
Description: Lemma for unified implication study. (Contributed by NM, 24-Dec-1997.)
Assertion
Ref Expression
u2lem7 (a2 (a2 b)) = (((ab ) ∪ (ab )) ∪ b)

Proof of Theorem u2lem7
StepHypRef Expression
1 df-i2 45 . 2 (a2 (a2 b)) = ((a2 b) ∪ (a ∩ (a2 b) ))
2 df-i2 45 . . . . 5 (a2 b) = (b ∪ (a b ))
3 ax-a1 30 . . . . . . . 8 a = a
43ax-r1 35 . . . . . . 7 a = a
54ran 78 . . . . . 6 (a b ) = (ab )
65lor 70 . . . . 5 (b ∪ (a b )) = (b ∪ (ab ))
72, 6ax-r2 36 . . . 4 (a2 b) = (b ∪ (ab ))
8 ancom 74 . . . . 5 (a ∩ (a2 b) ) = ((a2 b)a )
9 u2lemnaa 641 . . . . 5 ((a2 b)a ) = (ab )
108, 9ax-r2 36 . . . 4 (a ∩ (a2 b) ) = (ab )
117, 102or 72 . . 3 ((a2 b) ∪ (a ∩ (a2 b) )) = ((b ∪ (ab )) ∪ (ab ))
12 ax-a3 32 . . . 4 ((b ∪ (ab )) ∪ (ab )) = (b ∪ ((ab ) ∪ (ab )))
13 ax-a2 31 . . . 4 (b ∪ ((ab ) ∪ (ab ))) = (((ab ) ∪ (ab )) ∪ b)
1412, 13ax-r2 36 . . 3 ((b ∪ (ab )) ∪ (ab )) = (((ab ) ∪ (ab )) ∪ b)
1511, 14ax-r2 36 . 2 ((a2 b) ∪ (a ∩ (a2 b) )) = (((ab ) ∪ (ab )) ∪ b)
161, 15ax-r2 36 1 (a2 (a2 b)) = (((ab ) ∪ (ab )) ∪ b)
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  2 wi2 13
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38
This theorem depends on definitions:  df-a 40  df-i2 45  df-le1 130  df-le2 131
This theorem is referenced by:  u2lem7n  775  u2lem8  782
  Copyright terms: Public domain W3C validator