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

Theorem comanblem2 871
Description: Lemma for biconditional commutation law. (Contributed by NM, 1-Dec-1999.)
Assertion
Ref Expression
comanblem2 ((ab) ∩ ((ac) ∩ (bc))) = ((ab) ∩ c)

Proof of Theorem comanblem2
StepHypRef Expression
1 dfb 94 . . . 4 (ac) = ((ac) ∪ (ac ))
2 dfb 94 . . . 4 (bc) = ((bc) ∪ (bc ))
31, 22an 79 . . 3 ((ac) ∩ (bc)) = (((ac) ∪ (ac )) ∩ ((bc) ∪ (bc )))
43lan 77 . 2 ((ab) ∩ ((ac) ∩ (bc))) = ((ab) ∩ (((ac) ∪ (ac )) ∩ ((bc) ∪ (bc ))))
5 comanr1 464 . . . . . 6 a C (ac)
6 comanr1 464 . . . . . . 7 a C (ac )
76comcom6 459 . . . . . 6 a C (ac )
85, 7fh1 469 . . . . 5 (a ∩ ((ac) ∪ (ac ))) = ((a ∩ (ac)) ∪ (a ∩ (ac )))
9 anass 76 . . . . . . . 8 ((aa) ∩ c) = (a ∩ (ac))
109ax-r1 35 . . . . . . 7 (a ∩ (ac)) = ((aa) ∩ c)
11 anidm 111 . . . . . . . 8 (aa) = a
1211ran 78 . . . . . . 7 ((aa) ∩ c) = (ac)
1310, 12ax-r2 36 . . . . . 6 (a ∩ (ac)) = (ac)
14 dff 101 . . . . . . . . 9 0 = (aa )
1514ran 78 . . . . . . . 8 (0 ∩ c ) = ((aa ) ∩ c )
1615ax-r1 35 . . . . . . 7 ((aa ) ∩ c ) = (0 ∩ c )
17 anass 76 . . . . . . 7 ((aa ) ∩ c ) = (a ∩ (ac ))
18 an0r 109 . . . . . . 7 (0 ∩ c ) = 0
1916, 17, 183tr2 64 . . . . . 6 (a ∩ (ac )) = 0
2013, 192or 72 . . . . 5 ((a ∩ (ac)) ∪ (a ∩ (ac ))) = ((ac) ∪ 0)
21 or0 102 . . . . 5 ((ac) ∪ 0) = (ac)
228, 20, 213tr 65 . . . 4 (a ∩ ((ac) ∪ (ac ))) = (ac)
23 comanr1 464 . . . . . 6 b C (bc)
24 comanr1 464 . . . . . . 7 b C (bc )
2524comcom6 459 . . . . . 6 b C (bc )
2623, 25fh1 469 . . . . 5 (b ∩ ((bc) ∪ (bc ))) = ((b ∩ (bc)) ∪ (b ∩ (bc )))
27 anass 76 . . . . . . . 8 ((bb) ∩ c) = (b ∩ (bc))
2827ax-r1 35 . . . . . . 7 (b ∩ (bc)) = ((bb) ∩ c)
29 anidm 111 . . . . . . . 8 (bb) = b
3029ran 78 . . . . . . 7 ((bb) ∩ c) = (bc)
3128, 30ax-r2 36 . . . . . 6 (b ∩ (bc)) = (bc)
32 dff 101 . . . . . . . . 9 0 = (bb )
3332ran 78 . . . . . . . 8 (0 ∩ c ) = ((bb ) ∩ c )
3433ax-r1 35 . . . . . . 7 ((bb ) ∩ c ) = (0 ∩ c )
35 anass 76 . . . . . . 7 ((bb ) ∩ c ) = (b ∩ (bc ))
3634, 35, 183tr2 64 . . . . . 6 (b ∩ (bc )) = 0
3731, 362or 72 . . . . 5 ((b ∩ (bc)) ∪ (b ∩ (bc ))) = ((bc) ∪ 0)
38 or0 102 . . . . 5 ((bc) ∪ 0) = (bc)
3926, 37, 383tr 65 . . . 4 (b ∩ ((bc) ∪ (bc ))) = (bc)
4022, 392an 79 . . 3 ((a ∩ ((ac) ∪ (ac ))) ∩ (b ∩ ((bc) ∪ (bc )))) = ((ac) ∩ (bc))
41 an4 86 . . 3 ((ab) ∩ (((ac) ∪ (ac )) ∩ ((bc) ∪ (bc )))) = ((a ∩ ((ac) ∪ (ac ))) ∩ (b ∩ ((bc) ∪ (bc ))))
42 anandir 115 . . 3 ((ab) ∩ c) = ((ac) ∩ (bc))
4340, 41, 423tr1 63 . 2 ((ab) ∩ (((ac) ∪ (ac )) ∩ ((bc) ∪ (bc )))) = ((ab) ∩ c)
444, 43ax-r2 36 1 ((ab) ∩ ((ac) ∩ (bc))) = ((ab) ∩ c)
Colors of variables: term
Syntax hints:   = wb 1   wn 4  tb 5  wo 6  wa 7  0wf 9
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-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  comanb  872
  Copyright terms: Public domain W3C validator