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

Theorem u4lemanb 618
Description: Lemma for non-tollens implication study.
Assertion
Ref Expression
u4lemanb ((a4 b) ∩ b ) = ((ab) ∩ b )

Proof of Theorem u4lemanb
StepHypRef Expression
1 df-i4 47 . . 3 (a4 b) = (((ab) ∪ (ab)) ∪ ((ab) ∩ b ))
21ran 78 . 2 ((a4 b) ∩ b ) = ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∩ b )
3 comanr2 465 . . . . . 6 b C (ab)
43comcom3 454 . . . . 5 b C (ab)
5 comanr2 465 . . . . . 6 b C (ab)
65comcom3 454 . . . . 5 b C (ab)
74, 6com2or 483 . . . 4 b C ((ab) ∪ (ab))
8 comorr2 463 . . . . . 6 b C (ab)
98comcom3 454 . . . . 5 b C (ab)
10 comid 187 . . . . 5 b C b
119, 10com2an 484 . . . 4 b C ((ab) ∩ b )
127, 11fh1r 473 . . 3 ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∩ b ) = ((((ab) ∪ (ab)) ∩ b ) ∪ (((ab) ∩ b ) ∩ b ))
13 ax-a2 31 . . . 4 ((((ab) ∪ (ab)) ∩ b ) ∪ (((ab) ∩ b ) ∩ b )) = ((((ab) ∩ b ) ∩ b ) ∪ (((ab) ∪ (ab)) ∩ b ))
14 anass 76 . . . . . . 7 (((ab) ∩ b ) ∩ b ) = ((ab) ∩ (bb ))
15 anidm 111 . . . . . . . 8 (bb ) = b
1615lan 77 . . . . . . 7 ((ab) ∩ (bb )) = ((ab) ∩ b )
1714, 16ax-r2 36 . . . . . 6 (((ab) ∩ b ) ∩ b ) = ((ab) ∩ b )
184, 6fh1r 473 . . . . . . 7 (((ab) ∪ (ab)) ∩ b ) = (((ab) ∩ b ) ∪ ((ab) ∩ b ))
19 anass 76 . . . . . . . . . 10 ((ab) ∩ b ) = (a ∩ (bb ))
20 dff 101 . . . . . . . . . . . . 13 0 = (bb )
2120lan 77 . . . . . . . . . . . 12 (a ∩ 0) = (a ∩ (bb ))
2221ax-r1 35 . . . . . . . . . . 11 (a ∩ (bb )) = (a ∩ 0)
23 an0 108 . . . . . . . . . . 11 (a ∩ 0) = 0
2422, 23ax-r2 36 . . . . . . . . . 10 (a ∩ (bb )) = 0
2519, 24ax-r2 36 . . . . . . . . 9 ((ab) ∩ b ) = 0
26 anass 76 . . . . . . . . . 10 ((ab) ∩ b ) = (a ∩ (bb ))
2720lan 77 . . . . . . . . . . . 12 (a ∩ 0) = (a ∩ (bb ))
2827ax-r1 35 . . . . . . . . . . 11 (a ∩ (bb )) = (a ∩ 0)
29 an0 108 . . . . . . . . . . 11 (a ∩ 0) = 0
3028, 29ax-r2 36 . . . . . . . . . 10 (a ∩ (bb )) = 0
3126, 30ax-r2 36 . . . . . . . . 9 ((ab) ∩ b ) = 0
3225, 312or 72 . . . . . . . 8 (((ab) ∩ b ) ∪ ((ab) ∩ b )) = (0 ∪ 0)
33 or0 102 . . . . . . . 8 (0 ∪ 0) = 0
3432, 33ax-r2 36 . . . . . . 7 (((ab) ∩ b ) ∪ ((ab) ∩ b )) = 0
3518, 34ax-r2 36 . . . . . 6 (((ab) ∪ (ab)) ∩ b ) = 0
3617, 352or 72 . . . . 5 ((((ab) ∩ b ) ∩ b ) ∪ (((ab) ∪ (ab)) ∩ b )) = (((ab) ∩ b ) ∪ 0)
37 or0 102 . . . . 5 (((ab) ∩ b ) ∪ 0) = ((ab) ∩ b )
3836, 37ax-r2 36 . . . 4 ((((ab) ∩ b ) ∩ b ) ∪ (((ab) ∪ (ab)) ∩ b )) = ((ab) ∩ b )
3913, 38ax-r2 36 . . 3 ((((ab) ∪ (ab)) ∩ b ) ∪ (((ab) ∩ b ) ∩ b )) = ((ab) ∩ b )
4012, 39ax-r2 36 . 2 ((((ab) ∪ (ab)) ∪ ((ab) ∩ b )) ∩ b ) = ((ab) ∩ b )
412, 40ax-r2 36 1 ((a4 b) ∩ b ) = ((ab) ∩ b )
Colors of variables: term
Syntax hints:   = wb 1   wn 4  wo 6  wa 7  0wf 9  4 wi4 15
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i4 47  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  u4lemnob  673  u24lem  770
  Copyright terms: Public domain W3C validator