QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  u3lemax5 Unicode version
Theorem u3lemax5 797
Description: Possible axiom for Kalmbach implication system.
Assertion
Ref Expression
u3lemax5 ((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))))))) = 1
Proof of Theorem u3lemax5
StepHypRef Expression
1 lem4 511 . 2 ((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))))))) = ((a ->3 b)' v ((b ->3 a) ->3 ((b ->3 a) ->3 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))))))
2 lem4 511 . . . . 5 ((b ->3 a) ->3 ((b ->3 a) ->3 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))))) = ((b ->3 a)' v ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))))
3 lem4 511 . . . . . . 7 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))) = ((b ->3 c)' v ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))
4 lem4 511 . . . . . . . . 9 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))) = ((c ->3 b)' v (a ->3 c))
54lor 70 . . . . . . . 8 ((b ->3 c)' v ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c)))) = ((b ->3 c)' v ((c ->3 b)' v (a ->3 c)))
6 ax-a3 32 . . . . . . . . . 10 (((b ->3 c)' v (c ->3 b)') v (a ->3 c)) = ((b ->3 c)' v ((c ->3 b)' v (a ->3 c)))
76ax-r1 35 . . . . . . . . 9 ((b ->3 c)' v ((c ->3 b)' v (a ->3 c))) = (((b ->3 c)' v (c ->3 b)') v (a ->3 c))
8 oran3 93 . . . . . . . . . . 11 ((b ->3 c)' v (c ->3 b)') = ((b ->3 c) ^ (c ->3 b))'
9 u3lembi 723 . . . . . . . . . . . 12 ((b ->3 c) ^ (c ->3 b)) = (b == c)
109ax-r4 37 . . . . . . . . . . 11 ((b ->3 c) ^ (c ->3 b))' = (b == c)'
118, 10ax-r2 36 . . . . . . . . . 10 ((b ->3 c)' v (c ->3 b)') = (b == c)'
1211ax-r5 38 . . . . . . . . 9 (((b ->3 c)' v (c ->3 b)') v (a ->3 c)) = ((b == c)' v (a ->3 c))
137, 12ax-r2 36 . . . . . . . 8 ((b ->3 c)' v ((c ->3 b)' v (a ->3 c))) = ((b == c)' v (a ->3 c))
145, 13ax-r2 36 . . . . . . 7 ((b ->3 c)' v ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c)))) = ((b == c)' v (a ->3 c))
153, 14ax-r2 36 . . . . . 6 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))) = ((b == c)' v (a ->3 c))
1615lor 70 . . . . 5 ((b ->3 a)' v ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c)))))) = ((b ->3 a)' v ((b == c)' v (a ->3 c)))
172, 16ax-r2 36 . . . 4 ((b ->3 a) ->3 ((b ->3 a) ->3 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))))) = ((b ->3 a)' v ((b == c)' v (a ->3 c)))
1817lor 70 . . 3 ((a ->3 b)' v ((b ->3 a) ->3 ((b ->3 a) ->3 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c)))))))) = ((a ->3 b)' v ((b ->3 a)' v ((b == c)' v (a ->3 c))))
19 ax-a3 32 . . . . 5 (((a ->3 b)' v (b ->3 a)') v ((b == c)' v (a ->3 c))) = ((a ->3 b)' v ((b ->3 a)' v ((b == c)' v (a ->3 c))))
2019ax-r1 35 . . . 4 ((a ->3 b)' v ((b ->3 a)' v ((b == c)' v (a ->3 c)))) = (((a ->3 b)' v (b ->3 a)') v ((b == c)' v (a ->3 c)))
21 oran3 93 . . . . . . 7 ((a ->3 b)' v (b ->3 a)') = ((a ->3 b) ^ (b ->3 a))'
22 u3lembi 723 . . . . . . . 8 ((a ->3 b) ^ (b ->3 a)) = (a == b)
2322ax-r4 37 . . . . . . 7 ((a ->3 b) ^ (b ->3 a))' = (a == b)'
2421, 23ax-r2 36 . . . . . 6 ((a ->3 b)' v (b ->3 a)') = (a == b)'
2524ax-r5 38 . . . . 5 (((a ->3 b)' v (b ->3 a)') v ((b == c)' v (a ->3 c))) = ((a == b)' v ((b == c)' v (a ->3 c)))
26 le1 146 . . . . . 6 ((a == b)' v ((b == c)' v (a ->3 c))) =< 1
27 ska2 432 . . . . . . . 8 ((a == b)' v ((b == c)' v (a == c))) = 1
2827ax-r1 35 . . . . . . 7 1 = ((a == b)' v ((b == c)' v (a == c)))
29 u3lembi 723 . . . . . . . . . . 11 ((a ->3 c) ^ (c ->3 a)) = (a == c)
3029ax-r1 35 . . . . . . . . . 10 (a == c) = ((a ->3 c) ^ (c ->3 a))
31 lea 160 . . . . . . . . . 10 ((a ->3 c) ^ (c ->3 a)) =< (a ->3 c)
3230, 31bltr 138 . . . . . . . . 9 (a == c) =< (a ->3 c)
3332lelor 166 . . . . . . . 8 ((b == c)' v (a == c)) =< ((b == c)' v (a ->3 c))
3433lelor 166 . . . . . . 7 ((a == b)' v ((b == c)' v (a == c))) =< ((a == b)' v ((b == c)' v (a ->3 c)))
3528, 34bltr 138 . . . . . 6 1 =< ((a == b)' v ((b == c)' v (a ->3 c)))
3626, 35lebi 145 . . . . 5 ((a == b)' v ((b == c)' v (a ->3 c))) = 1
3725, 36ax-r2 36 . . . 4 (((a ->3 b)' v (b ->3 a)') v ((b == c)' v (a ->3 c))) = 1
3820, 37ax-r2 36 . . 3 ((a ->3 b)' v ((b ->3 a)' v ((b == c)' v (a ->3 c)))) = 1
3918, 38ax-r2 36 . 2 ((a ->3 b)' v ((b ->3 a) ->3 ((b ->3 a) ->3 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c)))))))) = 1
401, 39ax-r2 36 1 ((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((b ->3 c) ->3 ((b ->3 c) ->3 ((c ->3 b) ->3 ((c ->3 b) ->3 (a ->3 c))))))))) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8   ->3 wi3 14
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  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-i3 46  df-le 129  df-le1 130  df-le2 131  df-c1 132  df-c2 133  df-cmtr 134
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator