QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ka4ot Unicode version
Theorem ka4ot 435
Description: 3-variable version of weakly orthomodular law. It is proved from a weaker-looking equivalent, wom2 434, which in turn is proved from ax-wom 361.
Assertion
Ref Expression
ka4ot ((a == b)' v ((a v c) == (b v c))) = 1
Proof of Theorem ka4ot
StepHypRef Expression
1 le1 146 . 2 ((a == b)' v ((a v c) == (b v c))) =< 1
2 wom2 434 . . . . . 6 a =< ((a == b)' v ((a v c) == (b v c)))
3 wom2 434 . . . . . . 7 b =< ((b == a)' v ((b v c) == (a v c)))
4 bicom 96 . . . . . . . . 9 (b == a) = (a == b)
54ax-r4 37 . . . . . . . 8 (b == a)' = (a == b)'
6 bicom 96 . . . . . . . 8 ((b v c) == (a v c)) = ((a v c) == (b v c))
75, 62or 72 . . . . . . 7 ((b == a)' v ((b v c) == (a v c))) = ((a == b)' v ((a v c) == (b v c)))
83, 7lbtr 139 . . . . . 6 b =< ((a == b)' v ((a v c) == (b v c)))
92, 8le2or 168 . . . . 5 (a v b) =< (((a == b)' v ((a v c) == (b v c))) v ((a == b)' v ((a v c) == (b v c))))
10 oridm 110 . . . . 5 (((a == b)' v ((a v c) == (b v c))) v ((a == b)' v ((a v c) == (b v c)))) = ((a == b)' v ((a v c) == (b v c)))
119, 10lbtr 139 . . . 4 (a v b) =< ((a == b)' v ((a v c) == (b v c)))
1211leror 152 . . 3 ((a v b) v ((a v c) == (b v c))) =< (((a == b)' v ((a v c) == (b v c))) v ((a v c) == (b v c)))
13 ka4lemo 228 . . 3 ((a v b) v ((a v c) == (b v c))) = 1
14 ax-a3 32 . . . 4 (((a == b)' v ((a v c) == (b v c))) v ((a v c) == (b v c))) = ((a == b)' v (((a v c) == (b v c)) v ((a v c) == (b v c))))
15 oridm 110 . . . . 5 (((a v c) == (b v c)) v ((a v c) == (b v c))) = ((a v c) == (b v c))
1615lor 70 . . . 4 ((a == b)' v (((a v c) == (b v c)) v ((a v c) == (b v c)))) = ((a == b)' v ((a v c) == (b v c)))
1714, 16ax-r2 36 . . 3 (((a == b)' v ((a v c) == (b v c))) v ((a v c) == (b v c))) = ((a == b)' v ((a v c) == (b v c)))
1812, 13, 17le3tr2 141 . 2 1 =< ((a == b)' v ((a v c) == (b v c)))
191, 18lebi 145 1 ((a == b)' v ((a v c) == (b v c))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6  1wt 8
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-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-le 129  df-le1 130  df-le2 131  df-cmtr 134
This theorem is referenced by:  i3or  497
  Copyright terms: Public domain W3C validator