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

Theorem mldual 1122
 Description: Dual of modular law.
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 1121 . . . 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 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:  mldual2i  1125  vneulem13  1141  vneulemexp  1146  dp41lemd  1184  dp41leme  1185  dp32  1194  xdp41  1196  xxdp41  1199  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
 Copyright terms: Public domain W3C validator