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

Theorem l42modlem1 1147
 Description: Lemma for l42mod 1149..
Assertion
Ref Expression
l42modlem1 (((ab) ∪ d) ∩ ((ab) ∪ e)) = ((ab) ∪ ((ad) ∩ (be)))

Proof of Theorem l42modlem1
StepHypRef Expression
1 leo 158 . . . . . 6 b ≤ (be)
21ml2i 1123 . . . . 5 (b ∪ ((ad) ∩ (be))) = ((b ∪ (ad)) ∩ (be))
3 ancom 74 . . . . 5 ((b ∪ (ad)) ∩ (be)) = ((be) ∩ (b ∪ (ad)))
42, 3tr 62 . . . 4 (b ∪ ((ad) ∩ (be))) = ((be) ∩ (b ∪ (ad)))
54lor 70 . . 3 (a ∪ (b ∪ ((ad) ∩ (be)))) = (a ∪ ((be) ∩ (b ∪ (ad))))
65cm 61 . 2 (a ∪ ((be) ∩ (b ∪ (ad)))) = (a ∪ (b ∪ ((ad) ∩ (be))))
7 orass 75 . . . . 5 ((ab) ∪ d) = (a ∪ (bd))
8 or12 80 . . . . 5 (a ∪ (bd)) = (b ∪ (ad))
97, 8tr 62 . . . 4 ((ab) ∪ d) = (b ∪ (ad))
10 orass 75 . . . 4 ((ab) ∪ e) = (a ∪ (be))
119, 102an 79 . . 3 (((ab) ∪ d) ∩ ((ab) ∪ e)) = ((b ∪ (ad)) ∩ (a ∪ (be)))
12 ancom 74 . . 3 ((b ∪ (ad)) ∩ (a ∪ (be))) = ((a ∪ (be)) ∩ (b ∪ (ad)))
13 leo 158 . . . . . 6 a ≤ (ad)
1413lerr 150 . . . . 5 a ≤ (b ∪ (ad))
1514ml2i 1123 . . . 4 (a ∪ ((be) ∩ (b ∪ (ad)))) = ((a ∪ (be)) ∩ (b ∪ (ad)))
1615cm 61 . . 3 ((a ∪ (be)) ∩ (b ∪ (ad))) = (a ∪ ((be) ∩ (b ∪ (ad))))
1711, 12, 163tr 65 . 2 (((ab) ∪ d) ∩ ((ab) ∪ e)) = (a ∪ ((be) ∩ (b ∪ (ad))))
18 orass 75 . 2 ((ab) ∪ ((ad) ∩ (be))) = (a ∪ (b ∪ ((ad) ∩ (be))))
196, 17, 183tr1 63 1 (((ab) ∪ d) ∩ ((ab) ∪ e)) = ((ab) ∪ ((ad) ∩ (be)))
 Colors of variables: term Syntax hints:   = wb 1   ∪ wo 6   ∩ wa 7 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  ax-ml 1120 This theorem depends on definitions:  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131 This theorem is referenced by:  l42mod  1149  testmod2  1213  testmod2expanded  1214
 Copyright terms: Public domain W3C validator