QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ml2i Unicode version
Theorem ml2i 1123
Description: Inference version of modular law.
Hypothesis
Ref Expression
mli.1 c =< a
Assertion
Ref Expression
ml2i (c v (b ^ a)) = ((c v b) ^ a)
Proof of Theorem ml2i
StepHypRef Expression
1 ml 1121 . 2 (c v (b ^ (c v a))) = ((c v b) ^ (c v a))
2 mli.1 . . . . 5 c =< a
32df-le2 131 . . . 4 (c v a) = a
43lan 77 . . 3 (b ^ (c v a)) = (b ^ a)
54lor 70 . 2 (c v (b ^ (c v a))) = (c v (b ^ a))
63lan 77 . 2 ((c v b) ^ (c v a)) = ((c v b) ^ a)
71, 5, 63tr2 64 1 (c v (b ^ a)) = ((c v b) ^ a)
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2   v 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:  mli  1124  l42modlem1  1147  dp53lemb  1162  dp35lemb  1174  dp41lemd  1184  dp32  1194  xdp41  1196  xdp53  1198  xxdp41  1199  xxdp53  1201  xdp45lem  1202  xdp43lem  1203  xdp45  1204  xdp43  1205  3dp43  1206
  Copyright terms: Public domain W3C validator