QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  3vded22 Unicode version
Theorem 3vded22 818
Description: A 3-variable theorem. Experiment with weak deduction theorem.
Hypotheses
Ref Expression
3vded22.1 c =< ( C (a, b) v C (c, b))
3vded22.2 c =< a
3vded22.3 c =< (a ->0 b)
Assertion
Ref Expression
3vded22 c =< b
Proof of Theorem 3vded22
StepHypRef Expression
1 3vded22.1 . . . 4 c =< ( C (a, b) v C (c, b))
2 df-cmtr 134 . . . . . . 7 C (a, b) = (((a ^ b) v (a ^ b')) v ((a' ^ b) v (a' ^ b')))
3 or4 84 . . . . . . 7 (((a ^ b) v (a ^ b')) v ((a' ^ b) v (a' ^ b'))) = (((a ^ b) v (a' ^ b)) v ((a ^ b') v (a' ^ b')))
42, 3ax-r2 36 . . . . . 6 C (a, b) = (((a ^ b) v (a' ^ b)) v ((a ^ b') v (a' ^ b')))
5 lear 161 . . . . . . . 8 (a ^ b) =< b
6 lear 161 . . . . . . . 8 (a' ^ b) =< b
75, 6lel2or 170 . . . . . . 7 ((a ^ b) v (a' ^ b)) =< b
8 3vded22.2 . . . . . . . . . 10 c =< a
98lecon 154 . . . . . . . . 9 a' =< c'
109leran 153 . . . . . . . 8 (a' ^ b') =< (c' ^ b')
1110lelor 166 . . . . . . 7 ((a ^ b') v (a' ^ b')) =< ((a ^ b') v (c' ^ b'))
127, 11le2or 168 . . . . . 6 (((a ^ b) v (a' ^ b)) v ((a ^ b') v (a' ^ b'))) =< (b v ((a ^ b') v (c' ^ b')))
134, 12bltr 138 . . . . 5 C (a, b) =< (b v ((a ^ b') v (c' ^ b')))
14 df-cmtr 134 . . . . . . 7 C (c, b) = (((c ^ b) v (c ^ b')) v ((c' ^ b) v (c' ^ b')))
15 or4 84 . . . . . . 7 (((c ^ b) v (c ^ b')) v ((c' ^ b) v (c' ^ b'))) = (((c ^ b) v (c' ^ b)) v ((c ^ b') v (c' ^ b')))
1614, 15ax-r2 36 . . . . . 6 C (c, b) = (((c ^ b) v (c' ^ b)) v ((c ^ b') v (c' ^ b')))
17 lear 161 . . . . . . . 8 (c ^ b) =< b
18 lear 161 . . . . . . . 8 (c' ^ b) =< b
1917, 18lel2or 170 . . . . . . 7 ((c ^ b) v (c' ^ b)) =< b
208leran 153 . . . . . . . 8 (c ^ b') =< (a ^ b')
2120leror 152 . . . . . . 7 ((c ^ b') v (c' ^ b')) =< ((a ^ b') v (c' ^ b'))
2219, 21le2or 168 . . . . . 6 (((c ^ b) v (c' ^ b)) v ((c ^ b') v (c' ^ b'))) =< (b v ((a ^ b') v (c' ^ b')))
2316, 22bltr 138 . . . . 5 C (c, b) =< (b v ((a ^ b') v (c' ^ b')))
2413, 23le2or 168 . . . 4 ( C (a, b) v C (c, b)) =< ((b v ((a ^ b') v (c' ^ b'))) v (b v ((a ^ b') v (c' ^ b'))))
251, 24letr 137 . . 3 c =< ((b v ((a ^ b') v (c' ^ b'))) v (b v ((a ^ b') v (c' ^ b'))))
26 df-i0 43 . . . . 5 ((a ->0 b) ->0 (c ->2 b)) = ((a ->0 b)' v (c ->2 b))
27 or12 80 . . . . . 6 ((a ^ b') v (b v (c' ^ b'))) = (b v ((a ^ b') v (c' ^ b')))
28 df-i0 43 . . . . . . . . 9 (a ->0 b) = (a' v b)
2928ax-r4 37 . . . . . . . 8 (a ->0 b)' = (a' v b)'
30 anor1 88 . . . . . . . . 9 (a ^ b') = (a' v b)'
3130ax-r1 35 . . . . . . . 8 (a' v b)' = (a ^ b')
3229, 31ax-r2 36 . . . . . . 7 (a ->0 b)' = (a ^ b')
33 df-i2 45 . . . . . . 7 (c ->2 b) = (b v (c' ^ b'))
3432, 332or 72 . . . . . 6 ((a ->0 b)' v (c ->2 b)) = ((a ^ b') v (b v (c' ^ b')))
35 oridm 110 . . . . . 6 ((b v ((a ^ b') v (c' ^ b'))) v (b v ((a ^ b') v (c' ^ b')))) = (b v ((a ^ b') v (c' ^ b')))
3627, 34, 353tr1 63 . . . . 5 ((a ->0 b)' v (c ->2 b)) = ((b v ((a ^ b') v (c' ^ b'))) v (b v ((a ^ b') v (c' ^ b'))))
3726, 36ax-r2 36 . . . 4 ((a ->0 b) ->0 (c ->2 b)) = ((b v ((a ^ b') v (c' ^ b'))) v (b v ((a ^ b') v (c' ^ b'))))
3837ax-r1 35 . . 3 ((b v ((a ^ b') v (c' ^ b'))) v (b v ((a ^ b') v (c' ^ b')))) = ((a ->0 b) ->0 (c ->2 b))
3925, 38lbtr 139 . 2 c =< ((a ->0 b) ->0 (c ->2 b))
40 3vded22.3 . 2 c =< (a ->0 b)
4139, 403vded21 817 1 c =< b
Colors of variables: term
Syntax hints:   =< wle 2  'wn 4   v wo 6   ^ wa 7   ->0 wi0 11   ->2 wi2 13   C wcmtr 29
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  df-cmtr 134
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator