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

Theorem mldual2i 1125
 Description: Inference version of dual of modular law. (Contributed by NM, 1-Apr-2012.)
Hypothesis
Ref Expression
mlduali.1 ac
Assertion
Ref Expression
mldual2i (c ∩ (ba)) = ((cb) ∪ a)

Proof of Theorem mldual2i
StepHypRef Expression
1 mldual 1122 . 2 (c ∩ (b ∪ (ca))) = ((cb) ∪ (ca))
2 lear 161 . . . . 5 (ca) ≤ a
3 mlduali.1 . . . . . 6 ac
4 leid 148 . . . . . 6 aa
53, 4ler2an 173 . . . . 5 a ≤ (ca)
62, 5lebi 145 . . . 4 (ca) = a
76lor 70 . . 3 (b ∪ (ca)) = (ba)
87lan 77 . 2 (c ∩ (b ∪ (ca))) = (c ∩ (ba))
96lor 70 . 2 ((cb) ∪ (ca)) = ((cb) ∪ a)
101, 8, 93tr2 64 1 (c ∩ (ba)) = ((cb) ∪ a)
 Colors of variables: term Syntax hints:   = wb 1   ≤ wle 2   ∪ 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:  mlduali  1126  dp15lemf  1157  dp53lema  1161  dp53leme  1165  dp53lemf  1166  dp35lemd  1172  dp35lem0  1177  dp41lemc0  1182  dp41leme  1185  dp41lemk  1190  dp32  1194  xdp41  1196  xdp15  1197  xdp53  1198  xxdp41  1199  xxdp15  1200  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206  testmod2  1213  testmod2expanded  1214
 Copyright terms: Public domain W3C validator