QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  1oa Unicode version
Theorem 1oa 820
Description: Orthoarguesian-like law with ->1 instead of ->0 but true in all OMLs.
Assertion
Ref Expression
1oa ((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Proof of Theorem 1oa
StepHypRef Expression
1 lear 161 . . 3 ((((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v (b v (a' ^ b')))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c')))) =< ((a' ^ (b' ^ c')) v (c v (a' ^ c')))
2 an12 81 . . . . 5 (a' ^ (b' ^ c')) = (b' ^ (a' ^ c'))
3 lear 161 . . . . . 6 (b' ^ (a' ^ c')) =< (a' ^ c')
43lerr 150 . . . . 5 (b' ^ (a' ^ c')) =< (c v (a' ^ c'))
52, 4bltr 138 . . . 4 (a' ^ (b' ^ c')) =< (c v (a' ^ c'))
6 leid 148 . . . 4 (c v (a' ^ c')) =< (c v (a' ^ c'))
75, 6lel2or 170 . . 3 ((a' ^ (b' ^ c')) v (c v (a' ^ c'))) =< (c v (a' ^ c'))
81, 7letr 137 . 2 ((((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v (b v (a' ^ b')))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c')))) =< (c v (a' ^ c'))
9 df-i1 44 . . . 4 ((b v c) ->1 ((a ->2 b) ^ (a ->2 c))) = ((b v c)' v ((b v c) ^ ((a ->2 b) ^ (a ->2 c))))
109lan 77 . . 3 ((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) = ((a ->2 b) ^ ((b v c)' v ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))))
11 an12 81 . . . . . 6 ((a ->2 b) ^ ((b v c) ^ (a ->2 c))) = ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))
1211ax-r1 35 . . . . 5 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) = ((a ->2 b) ^ ((b v c) ^ (a ->2 c)))
13 coman1 185 . . . . 5 ((a ->2 b) ^ ((b v c) ^ (a ->2 c))) C (a ->2 b)
1412, 13bctr 181 . . . 4 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (a ->2 b)
15 coman1 185 . . . . 5 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (b v c)
1615comcom2 183 . . . 4 ((b v c) ^ ((a ->2 b) ^ (a ->2 c))) C (b v c)'
1714, 16fh2c 477 . . 3 ((a ->2 b) ^ ((b v c)' v ((b v c) ^ ((a ->2 b) ^ (a ->2 c))))) = (((a ->2 b) ^ (b v c)') v ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))))
18 df-i2 45 . . . . . . 7 (a ->2 b) = (b v (a' ^ b'))
19 anor3 90 . . . . . . . 8 (b' ^ c') = (b v c)'
2019ax-r1 35 . . . . . . 7 (b v c)' = (b' ^ c')
2118, 202an 79 . . . . . 6 ((a ->2 b) ^ (b v c)') = ((b v (a' ^ b')) ^ (b' ^ c'))
22 comid 187 . . . . . . . . . . 11 b C b
2322comcom3 454 . . . . . . . . . 10 b' C b
24 comanr2 465 . . . . . . . . . 10 b' C (a' ^ b')
2523, 24fh1r 473 . . . . . . . . 9 ((b v (a' ^ b')) ^ b') = ((b ^ b') v ((a' ^ b') ^ b'))
26 dff 101 . . . . . . . . . . 11 0 = (b ^ b')
2726ax-r1 35 . . . . . . . . . 10 (b ^ b') = 0
28 anass 76 . . . . . . . . . . 11 ((a' ^ b') ^ b') = (a' ^ (b' ^ b'))
29 anidm 111 . . . . . . . . . . . 12 (b' ^ b') = b'
3029lan 77 . . . . . . . . . . 11 (a' ^ (b' ^ b')) = (a' ^ b')
3128, 30ax-r2 36 . . . . . . . . . 10 ((a' ^ b') ^ b') = (a' ^ b')
3227, 312or 72 . . . . . . . . 9 ((b ^ b') v ((a' ^ b') ^ b')) = (0 v (a' ^ b'))
33 ax-a2 31 . . . . . . . . . 10 (0 v (a' ^ b')) = ((a' ^ b') v 0)
34 or0 102 . . . . . . . . . 10 ((a' ^ b') v 0) = (a' ^ b')
3533, 34ax-r2 36 . . . . . . . . 9 (0 v (a' ^ b')) = (a' ^ b')
3625, 32, 353tr 65 . . . . . . . 8 ((b v (a' ^ b')) ^ b') = (a' ^ b')
3736ran 78 . . . . . . 7 (((b v (a' ^ b')) ^ b') ^ c') = ((a' ^ b') ^ c')
38 anass 76 . . . . . . 7 (((b v (a' ^ b')) ^ b') ^ c') = ((b v (a' ^ b')) ^ (b' ^ c'))
39 anass 76 . . . . . . 7 ((a' ^ b') ^ c') = (a' ^ (b' ^ c'))
4037, 38, 393tr2 64 . . . . . 6 ((b v (a' ^ b')) ^ (b' ^ c')) = (a' ^ (b' ^ c'))
4121, 40ax-r2 36 . . . . 5 ((a ->2 b) ^ (b v c)') = (a' ^ (b' ^ c'))
42 an12 81 . . . . . 6 ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))) = ((b v c) ^ ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))))
43 anass 76 . . . . . . . . 9 (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c)) = ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c)))
4443ax-r1 35 . . . . . . . 8 ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) = (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c))
45 anidm 111 . . . . . . . . . 10 ((a ->2 b) ^ (a ->2 b)) = (a ->2 b)
4645, 18ax-r2 36 . . . . . . . . 9 ((a ->2 b) ^ (a ->2 b)) = (b v (a' ^ b'))
47 df-i2 45 . . . . . . . . 9 (a ->2 c) = (c v (a' ^ c'))
4846, 472an 79 . . . . . . . 8 (((a ->2 b) ^ (a ->2 b)) ^ (a ->2 c)) = ((b v (a' ^ b')) ^ (c v (a' ^ c')))
4944, 48ax-r2 36 . . . . . . 7 ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c))) = ((b v (a' ^ b')) ^ (c v (a' ^ c')))
5049lan 77 . . . . . 6 ((b v c) ^ ((a ->2 b) ^ ((a ->2 b) ^ (a ->2 c)))) = ((b v c) ^ ((b v (a' ^ b')) ^ (c v (a' ^ c'))))
5142, 50ax-r2 36 . . . . 5 ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c)))) = ((b v c) ^ ((b v (a' ^ b')) ^ (c v (a' ^ c'))))
5241, 512or 72 . . . 4 (((a ->2 b) ^ (b v c)') v ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c))))) = ((a' ^ (b' ^ c')) v ((b v c) ^ ((b v (a' ^ b')) ^ (c v (a' ^ c')))))
5339ax-r1 35 . . . . . . . 8 (a' ^ (b' ^ c')) = ((a' ^ b') ^ c')
54 lea 160 . . . . . . . . . 10 ((a' ^ b') ^ c') =< (a' ^ b')
5554lerr 150 . . . . . . . . 9 ((a' ^ b') ^ c') =< (b v (a' ^ b'))
5655lecom 180 . . . . . . . 8 ((a' ^ b') ^ c') C (b v (a' ^ b'))
5753, 56bctr 181 . . . . . . 7 (a' ^ (b' ^ c')) C (b v (a' ^ b'))
584lecom 180 . . . . . . . 8 (b' ^ (a' ^ c')) C (c v (a' ^ c'))
592, 58bctr 181 . . . . . . 7 (a' ^ (b' ^ c')) C (c v (a' ^ c'))
6057, 59fh3 471 . . . . . 6 ((a' ^ (b' ^ c')) v ((b v (a' ^ b')) ^ (c v (a' ^ c')))) = (((a' ^ (b' ^ c')) v (b v (a' ^ b'))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c'))))
6160lan 77 . . . . 5 (((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v ((b v (a' ^ b')) ^ (c v (a' ^ c'))))) = (((a' ^ (b' ^ c')) v (b v c)) ^ (((a' ^ (b' ^ c')) v (b v (a' ^ b'))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c')))))
62 coman2 186 . . . . . . . 8 (a' ^ (b' ^ c')) C (b' ^ c')
6362comcom2 183 . . . . . . 7 (a' ^ (b' ^ c')) C (b' ^ c')'
64 oran 87 . . . . . . . 8 (b v c) = (b' ^ c')'
6564ax-r1 35 . . . . . . 7 (b' ^ c')' = (b v c)
6663, 65cbtr 182 . . . . . 6 (a' ^ (b' ^ c')) C (b v c)
6757, 59com2an 484 . . . . . 6 (a' ^ (b' ^ c')) C ((b v (a' ^ b')) ^ (c v (a' ^ c')))
6866, 67fh3 471 . . . . 5 ((a' ^ (b' ^ c')) v ((b v c) ^ ((b v (a' ^ b')) ^ (c v (a' ^ c'))))) = (((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v ((b v (a' ^ b')) ^ (c v (a' ^ c')))))
69 anass 76 . . . . 5 ((((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v (b v (a' ^ b')))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c')))) = (((a' ^ (b' ^ c')) v (b v c)) ^ (((a' ^ (b' ^ c')) v (b v (a' ^ b'))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c')))))
7061, 68, 693tr1 63 . . . 4 ((a' ^ (b' ^ c')) v ((b v c) ^ ((b v (a' ^ b')) ^ (c v (a' ^ c'))))) = ((((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v (b v (a' ^ b')))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c'))))
7152, 70ax-r2 36 . . 3 (((a ->2 b) ^ (b v c)') v ((a ->2 b) ^ ((b v c) ^ ((a ->2 b) ^ (a ->2 c))))) = ((((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v (b v (a' ^ b')))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c'))))
7210, 17, 713tr 65 . 2 ((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) = ((((a' ^ (b' ^ c')) v (b v c)) ^ ((a' ^ (b' ^ c')) v (b v (a' ^ b')))) ^ ((a' ^ (b' ^ c')) v (c v (a' ^ c'))))
738, 72, 47le3tr1 140 1 ((a ->2 b) ^ ((b v c) ->1 ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 c)
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7  0wf 9   ->1 wi1 12   ->2 wi2 13
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:  1oai1  821  1oaiii  823  distoa  944
  Copyright terms: Public domain W3C validator