QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  u3lemax4 Unicode version
Theorem u3lemax4 796
Description: Possible axiom for Kalmbach implication system.
Assertion
Ref Expression
u3lemax4 ((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))))) = 1
Proof of Theorem u3lemax4
StepHypRef Expression
1 lem4 511 . 2 ((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))))) = ((a ->3 b)' v ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))))
2 lem4 511 . . . . 5 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))) = ((b ->3 a)' v ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))
3 lem4 511 . . . . . . 7 (c ->3 (c ->3 a)) = (c' v a)
4 lem4 511 . . . . . . 7 (c ->3 (c ->3 b)) = (c' v b)
53, 42i3 254 . . . . . 6 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))) = ((c' v a) ->3 (c' v b))
65lor 70 . . . . 5 ((b ->3 a)' v ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b)))) = ((b ->3 a)' v ((c' v a) ->3 (c' v b)))
72, 6ax-r2 36 . . . 4 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))) = ((b ->3 a)' v ((c' v a) ->3 (c' v b)))
87lor 70 . . 3 ((a ->3 b)' v ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b)))))) = ((a ->3 b)' v ((b ->3 a)' v ((c' v a) ->3 (c' v b))))
9 oran3 93 . . . . . 6 ((a ->3 b)' v (b ->3 a)') = ((a ->3 b) ^ (b ->3 a))'
10 u3lembi 723 . . . . . . 7 ((a ->3 b) ^ (b ->3 a)) = (a == b)
1110ax-r4 37 . . . . . 6 ((a ->3 b) ^ (b ->3 a))' = (a == b)'
129, 11ax-r2 36 . . . . 5 ((a ->3 b)' v (b ->3 a)') = (a == b)'
1312ax-r5 38 . . . 4 (((a ->3 b)' v (b ->3 a)') v ((c' v a) ->3 (c' v b))) = ((a == b)' v ((c' v a) ->3 (c' v b)))
14 ax-a3 32 . . . 4 (((a ->3 b)' v (b ->3 a)') v ((c' v a) ->3 (c' v b))) = ((a ->3 b)' v ((b ->3 a)' v ((c' v a) ->3 (c' v b))))
15 le1 146 . . . . 5 ((a == b)' v ((c' v a) ->3 (c' v b))) =< 1
16 ska4 433 . . . . . . . 8 ((a' == b')' v ((a' ^ c) == (b' ^ c))) = 1
1716ax-r1 35 . . . . . . 7 1 = ((a' == b')' v ((a' ^ c) == (b' ^ c)))
18 conb 122 . . . . . . . . . 10 (a == b) = (a' == b')
1918ax-r4 37 . . . . . . . . 9 (a == b)' = (a' == b')'
20 conb 122 . . . . . . . . . 10 ((c' v a) == (c' v b)) = ((c' v a)' == (c' v b)')
21 ancom 74 . . . . . . . . . . . . 13 (a' ^ c) = (c ^ a')
22 anor1 88 . . . . . . . . . . . . 13 (c ^ a') = (c' v a)'
2321, 22ax-r2 36 . . . . . . . . . . . 12 (a' ^ c) = (c' v a)'
24 ancom 74 . . . . . . . . . . . . 13 (b' ^ c) = (c ^ b')
25 anor1 88 . . . . . . . . . . . . 13 (c ^ b') = (c' v b)'
2624, 25ax-r2 36 . . . . . . . . . . . 12 (b' ^ c) = (c' v b)'
2723, 262bi 99 . . . . . . . . . . 11 ((a' ^ c) == (b' ^ c)) = ((c' v a)' == (c' v b)')
2827ax-r1 35 . . . . . . . . . 10 ((c' v a)' == (c' v b)') = ((a' ^ c) == (b' ^ c))
2920, 28ax-r2 36 . . . . . . . . 9 ((c' v a) == (c' v b)) = ((a' ^ c) == (b' ^ c))
3019, 292or 72 . . . . . . . 8 ((a == b)' v ((c' v a) == (c' v b))) = ((a' == b')' v ((a' ^ c) == (b' ^ c)))
3130ax-r1 35 . . . . . . 7 ((a' == b')' v ((a' ^ c) == (b' ^ c))) = ((a == b)' v ((c' v a) == (c' v b)))
3217, 31ax-r2 36 . . . . . 6 1 = ((a == b)' v ((c' v a) == (c' v b)))
33 u3lembi 723 . . . . . . . . 9 (((c' v a) ->3 (c' v b)) ^ ((c' v b) ->3 (c' v a))) = ((c' v a) == (c' v b))
3433ax-r1 35 . . . . . . . 8 ((c' v a) == (c' v b)) = (((c' v a) ->3 (c' v b)) ^ ((c' v b) ->3 (c' v a)))
35 lea 160 . . . . . . . 8 (((c' v a) ->3 (c' v b)) ^ ((c' v b) ->3 (c' v a))) =< ((c' v a) ->3 (c' v b))
3634, 35bltr 138 . . . . . . 7 ((c' v a) == (c' v b)) =< ((c' v a) ->3 (c' v b))
3736lelor 166 . . . . . 6 ((a == b)' v ((c' v a) == (c' v b))) =< ((a == b)' v ((c' v a) ->3 (c' v b)))
3832, 37bltr 138 . . . . 5 1 =< ((a == b)' v ((c' v a) ->3 (c' v b)))
3915, 38lebi 145 . . . 4 ((a == b)' v ((c' v a) ->3 (c' v b))) = 1
4013, 14, 393tr2 64 . . 3 ((a ->3 b)' v ((b ->3 a)' v ((c' v a) ->3 (c' v b)))) = 1
418, 40ax-r2 36 . 2 ((a ->3 b)' v ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b)))))) = 1
421, 41ax-r2 36 1 ((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))))) = 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