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

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

Proof of Theorem ml2i
StepHypRef Expression
1 ml 1123 . 2 (c ∪ (b ∩ (ca))) = ((cb) ∩ (ca))
2 mli.1 . . . . 5 ca
32df-le2 131 . . . 4 (ca) = a
43lan 77 . . 3 (b ∩ (ca)) = (ba)
54lor 70 . 2 (c ∪ (b ∩ (ca))) = (c ∪ (ba))
63lan 77 . 2 ((cb) ∩ (ca)) = ((cb) ∩ a)
71, 5, 63tr2 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 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:  mli  1126  l42modlem1  1149  dp53lemb  1164  dp35lemb  1176  dp41lemd  1186  dp32  1196  xdp41  1198  xdp53  1200  xxdp41  1201  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208
 Copyright terms: Public domain W3C validator