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

Theorem mldual 1124
 Description: Dual of modular law. (Contributed by NM, 15-Mar-2010.) (Revised by NM, 31-Mar-2011.)
Assertion
Ref Expression
mldual (a ∩ (b ∪ (ac))) = ((ab) ∪ (ac))

Proof of Theorem mldual
StepHypRef Expression
1 anor3 90 . . . . . . 7 (b ∩ (ac) ) = (b ∪ (ac))
21cm 61 . . . . . 6 (b ∪ (ac)) = (b ∩ (ac) )
3 oran3 93 . . . . . . . 8 (ac ) = (ac)
43lan 77 . . . . . . 7 (b ∩ (ac )) = (b ∩ (ac) )
54ax-r1 35 . . . . . 6 (b ∩ (ac) ) = (b ∩ (ac ))
62, 5tr 62 . . . . 5 (b ∪ (ac)) = (b ∩ (ac ))
76lor 70 . . . 4 (a ∪ (b ∪ (ac)) ) = (a ∪ (b ∩ (ac )))
8 ml 1123 . . . 4 (a ∪ (b ∩ (ac ))) = ((ab ) ∩ (ac ))
9 oran3 93 . . . . 5 (ab ) = (ab)
109, 32an 79 . . . 4 ((ab ) ∩ (ac )) = ((ab) ∩ (ac) )
117, 8, 103tr 65 . . 3 (a ∪ (b ∪ (ac)) ) = ((ab) ∩ (ac) )
12 oran3 93 . . 3 (a ∪ (b ∪ (ac)) ) = (a ∩ (b ∪ (ac)))
13 anor3 90 . . 3 ((ab) ∩ (ac) ) = ((ab) ∪ (ac))
1411, 12, 133tr2 64 . 2 (a ∩ (b ∪ (ac))) = ((ab) ∪ (ac))
1514con1 66 1 (a ∩ (b ∪ (ac))) = ((ab) ∪ (ac))
 Colors of variables: term Syntax hints:   = wb 1  ⊥ wn 4   ∪ 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 1122 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:  mldual2i  1127  vneulem13  1143  vneulemexp  1148  dp41lemd  1186  dp41leme  1187  dp32  1196  xdp41  1198  xxdp41  1201  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208
 Copyright terms: Public domain W3C validator