QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  3vded21 Unicode version
Theorem 3vded21 817
Description: A 3-variable theorem. Experiment with weak deduction theorem.
Hypotheses
Ref Expression
3vded21.1 c =< ((a ->0 b) ->0 (c ->2 b))
3vded21.2 c =< (a ->0 b)
Assertion
Ref Expression
3vded21 c =< b
Proof of Theorem 3vded21
StepHypRef Expression
1 3vded21.2 . . . . . . 7 c =< (a ->0 b)
2 df-i0 43 . . . . . . 7 (a ->0 b) = (a' v b)
31, 2lbtr 139 . . . . . 6 c =< (a' v b)
4 3vded21.1 . . . . . . 7 c =< ((a ->0 b) ->0 (c ->2 b))
5 df-i0 43 . . . . . . . 8 ((a ->0 b) ->0 (c ->2 b)) = ((a ->0 b)' v (c ->2 b))
62ax-r4 37 . . . . . . . . 9 (a ->0 b)' = (a' v b)'
7 df-i2 45 . . . . . . . . . 10 (c ->2 b) = (b v (c' ^ b'))
8 anor3 90 . . . . . . . . . . 11 (c' ^ b') = (c v b)'
98lor 70 . . . . . . . . . 10 (b v (c' ^ b')) = (b v (c v b)')
107, 9ax-r2 36 . . . . . . . . 9 (c ->2 b) = (b v (c v b)')
116, 102or 72 . . . . . . . 8 ((a ->0 b)' v (c ->2 b)) = ((a' v b)' v (b v (c v b)'))
12 ax-a2 31 . . . . . . . 8 ((a' v b)' v (b v (c v b)')) = ((b v (c v b)') v (a' v b)')
135, 11, 123tr 65 . . . . . . 7 ((a ->0 b) ->0 (c ->2 b)) = ((b v (c v b)') v (a' v b)')
144, 13lbtr 139 . . . . . 6 c =< ((b v (c v b)') v (a' v b)')
153, 14ler2an 173 . . . . 5 c =< ((a' v b) ^ ((b v (c v b)') v (a' v b)'))
16 comor2 462 . . . . . . . 8 (a' v b) C b
173leror 152 . . . . . . . . . . . 12 (c v b) =< ((a' v b) v b)
18 ax-a3 32 . . . . . . . . . . . . 13 ((a' v b) v b) = (a' v (b v b))
19 oridm 110 . . . . . . . . . . . . . 14 (b v b) = b
2019lor 70 . . . . . . . . . . . . 13 (a' v (b v b)) = (a' v b)
2118, 20ax-r2 36 . . . . . . . . . . . 12 ((a' v b) v b) = (a' v b)
2217, 21lbtr 139 . . . . . . . . . . 11 (c v b) =< (a' v b)
2322lecom 180 . . . . . . . . . 10 (c v b) C (a' v b)
2423comcom 453 . . . . . . . . 9 (a' v b) C (c v b)
2524comcom2 183 . . . . . . . 8 (a' v b) C (c v b)'
2616, 25com2or 483 . . . . . . 7 (a' v b) C (b v (c v b)')
27 comid 187 . . . . . . . 8 (a' v b) C (a' v b)
2827comcom2 183 . . . . . . 7 (a' v b) C (a' v b)'
2926, 28fh1 469 . . . . . 6 ((a' v b) ^ ((b v (c v b)') v (a' v b)')) = (((a' v b) ^ (b v (c v b)')) v ((a' v b) ^ (a' v b)'))
30 or0 102 . . . . . . 7 ((((a' v b) ^ b) v ((a' v b) ^ (c v b)')) v 0) = (((a' v b) ^ b) v ((a' v b) ^ (c v b)'))
3116, 25fh1 469 . . . . . . . . 9 ((a' v b) ^ (b v (c v b)')) = (((a' v b) ^ b) v ((a' v b) ^ (c v b)'))
3231ax-r1 35 . . . . . . . 8 (((a' v b) ^ b) v ((a' v b) ^ (c v b)')) = ((a' v b) ^ (b v (c v b)'))
33 dff 101 . . . . . . . 8 0 = ((a' v b) ^ (a' v b)')
3432, 332or 72 . . . . . . 7 ((((a' v b) ^ b) v ((a' v b) ^ (c v b)')) v 0) = (((a' v b) ^ (b v (c v b)')) v ((a' v b) ^ (a' v b)'))
35 ax-a2 31 . . . . . . . . . 10 (a' v b) = (b v a')
3635ran 78 . . . . . . . . 9 ((a' v b) ^ b) = ((b v a') ^ b)
37 ancom 74 . . . . . . . . 9 ((b v a') ^ b) = (b ^ (b v a'))
38 anabs 121 . . . . . . . . 9 (b ^ (b v a')) = b
3936, 37, 383tr 65 . . . . . . . 8 ((a' v b) ^ b) = b
4039ax-r5 38 . . . . . . 7 (((a' v b) ^ b) v ((a' v b) ^ (c v b)')) = (b v ((a' v b) ^ (c v b)'))
4130, 34, 403tr2 64 . . . . . 6 (((a' v b) ^ (b v (c v b)')) v ((a' v b) ^ (a' v b)')) = (b v ((a' v b) ^ (c v b)'))
4229, 41ax-r2 36 . . . . 5 ((a' v b) ^ ((b v (c v b)') v (a' v b)')) = (b v ((a' v b) ^ (c v b)'))
4315, 42lbtr 139 . . . 4 c =< (b v ((a' v b) ^ (c v b)'))
4443leran 153 . . 3 (c ^ (c v b)) =< ((b v ((a' v b) ^ (c v b)')) ^ (c v b))
45 anabs 121 . . 3 (c ^ (c v b)) = c
46 comor2 462 . . . . 5 (c v b) C b
47 comid 187 . . . . . . 7 (c v b) C (c v b)
4847comcom2 183 . . . . . 6 (c v b) C (c v b)'
4923, 48com2an 484 . . . . 5 (c v b) C ((a' v b) ^ (c v b)')
5046, 49fh1r 473 . . . 4 ((b v ((a' v b) ^ (c v b)')) ^ (c v b)) = ((b ^ (c v b)) v (((a' v b) ^ (c v b)') ^ (c v b)))
51 ax-a2 31 . . . . . . 7 (c v b) = (b v c)
5251lan 77 . . . . . 6 (b ^ (c v b)) = (b ^ (b v c))
53 anabs 121 . . . . . 6 (b ^ (b v c)) = b
5452, 53ax-r2 36 . . . . 5 (b ^ (c v b)) = b
55 an32 83 . . . . . 6 (((a' v b) ^ (c v b)') ^ (c v b)) = (((a' v b) ^ (c v b)) ^ (c v b)')
56 anass 76 . . . . . 6 (((a' v b) ^ (c v b)) ^ (c v b)') = ((a' v b) ^ ((c v b) ^ (c v b)'))
57 dff 101 . . . . . . . . 9 0 = ((c v b) ^ (c v b)')
5857lan 77 . . . . . . . 8 ((a' v b) ^ 0) = ((a' v b) ^ ((c v b) ^ (c v b)'))
5958ax-r1 35 . . . . . . 7 ((a' v b) ^ ((c v b) ^ (c v b)')) = ((a' v b) ^ 0)
60 an0 108 . . . . . . 7 ((a' v b) ^ 0) = 0
6159, 60ax-r2 36 . . . . . 6 ((a' v b) ^ ((c v b) ^ (c v b)')) = 0
6255, 56, 613tr 65 . . . . 5 (((a' v b) ^ (c v b)') ^ (c v b)) = 0
6354, 622or 72 . . . 4 ((b ^ (c v b)) v (((a' v b) ^ (c v b)') ^ (c v b))) = (b v 0)
6450, 63ax-r2 36 . . 3 ((b v ((a' v b) ^ (c v b)')) ^ (c v b)) = (b v 0)
6544, 45, 64le3tr2 141 . 2 c =< (b v 0)
66 or0 102 . 2 (b v 0) = b
6765, 66lbtr 139 1 c =< b
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7  0wf 9   ->0 wi0 11   ->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-i0 43  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  3vded22  818
  Copyright terms: Public domain W3C validator