QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  distid Unicode version
Theorem distid 887
Description: Distributive law for identity.
Assertion
Ref Expression
distid ((a == b) ^ ((a == c) v (b == c))) = (((a == b) ^ (a == c)) v ((a == b) ^ (b == c)))
Proof of Theorem distid
StepHypRef Expression
1 lea 160 . . . 4 ((a == b) ^ ((a == c) v (b == c))) =< (a == b)
2 mlaconjo 886 . . . 4 ((a == b) ^ ((a == c) v (b == c))) =< (a == c)
31, 2ler2an 173 . . 3 ((a == b) ^ ((a == c) v (b == c))) =< ((a == b) ^ (a == c))
4 bicom 96 . . . . . 6 (a == b) = (b == a)
5 ax-a2 31 . . . . . 6 ((a == c) v (b == c)) = ((b == c) v (a == c))
64, 52an 79 . . . . 5 ((a == b) ^ ((a == c) v (b == c))) = ((b == a) ^ ((b == c) v (a == c)))
7 mlaconjo 886 . . . . 5 ((b == a) ^ ((b == c) v (a == c))) =< (b == c)
86, 7bltr 138 . . . 4 ((a == b) ^ ((a == c) v (b == c))) =< (b == c)
91, 8ler2an 173 . . 3 ((a == b) ^ ((a == c) v (b == c))) =< ((a == b) ^ (b == c))
103, 9ler2or 172 . 2 ((a == b) ^ ((a == c) v (b == c))) =< (((a == b) ^ (a == c)) v ((a == b) ^ (b == c)))
11 ledi 174 . 2 (((a == b) ^ (a == c)) v ((a == b) ^ (b == c))) =< ((a == b) ^ ((a == c) v (b == c)))
1210, 11lebi 145 1 ((a == b) ^ ((a == c) v (b == c))) = (((a == b) ^ (a == c)) v ((a == b) ^ (b == c)))
Colors of variables: term
Syntax hints:   = wb 1   == tb 5   v wo 6   ^ wa 7
This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator