QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  3vroa Unicode version
Theorem 3vroa 831
Description: OA-like inference rule (requires OM only).
Hypothesis
Ref Expression
3vroa.1 ((a ->2 b) ^ ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))) = 1
Assertion
Ref Expression
3vroa (a ->2 c) = 1
Proof of Theorem 3vroa
StepHypRef Expression
1 df-i2 45 . 2 (a ->2 c) = (c v (a' ^ c'))
2 or12 80 . . 3 (c v ((a' ^ c') v (a' ^ c'))) = ((a' ^ c') v (c v (a' ^ c')))
3 oridm 110 . . . 4 ((a' ^ c') v (a' ^ c')) = (a' ^ c')
43lor 70 . . 3 (c v ((a' ^ c') v (a' ^ c'))) = (c v (a' ^ c'))
5 le1 146 . . . . . . . . . 10 (a ->2 b) =< 1
6 3vroa.1 . . . . . . . . . . . 12 ((a ->2 b) ^ ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))) = 1
76ax-r1 35 . . . . . . . . . . 11 1 = ((a ->2 b) ^ ((b v c) ->0 ((a ->2 b) ^ (a ->2 c))))
8 lea 160 . . . . . . . . . . 11 ((a ->2 b) ^ ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))) =< (a ->2 b)
97, 8bltr 138 . . . . . . . . . 10 1 =< (a ->2 b)
105, 9lebi 145 . . . . . . . . 9 (a ->2 b) = 1
1110ran 78 . . . . . . . 8 ((a ->2 b) ^ (a ->2 c)) = (1 ^ (a ->2 c))
12 ancom 74 . . . . . . . 8 (1 ^ (a ->2 c)) = ((a ->2 c) ^ 1)
1311, 12ax-r2 36 . . . . . . 7 ((a ->2 b) ^ (a ->2 c)) = ((a ->2 c) ^ 1)
14 an1 106 . . . . . . 7 ((a ->2 c) ^ 1) = (a ->2 c)
1513, 14, 13tr 65 . . . . . 6 ((a ->2 b) ^ (a ->2 c)) = (c v (a' ^ c'))
1615lor 70 . . . . 5 ((a' ^ c') v ((a ->2 b) ^ (a ->2 c))) = ((a' ^ c') v (c v (a' ^ c')))
1716ax-r1 35 . . . 4 ((a' ^ c') v (c v (a' ^ c'))) = ((a' ^ c') v ((a ->2 b) ^ (a ->2 c)))
18 le1 146 . . . . 5 ((a' ^ c') v ((a ->2 b) ^ (a ->2 c))) =< 1
19 lear 161 . . . . . . . 8 ((a ->2 b) ^ ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))) =< ((b v c) ->0 ((a ->2 b) ^ (a ->2 c)))
20 df-i0 43 . . . . . . . . 9 ((b v c) ->0 ((a ->2 b) ^ (a ->2 c))) = ((b v c)' v ((a ->2 b) ^ (a ->2 c)))
21 anor3 90 . . . . . . . . . . 11 (b' ^ c') = (b v c)'
2221ax-r5 38 . . . . . . . . . 10 ((b' ^ c') v ((a ->2 b) ^ (a ->2 c))) = ((b v c)' v ((a ->2 b) ^ (a ->2 c)))
2322ax-r1 35 . . . . . . . . 9 ((b v c)' v ((a ->2 b) ^ (a ->2 c))) = ((b' ^ c') v ((a ->2 b) ^ (a ->2 c)))
2420, 23ax-r2 36 . . . . . . . 8 ((b v c) ->0 ((a ->2 b) ^ (a ->2 c))) = ((b' ^ c') v ((a ->2 b) ^ (a ->2 c)))
2519, 6, 24le3tr2 141 . . . . . . 7 1 =< ((b' ^ c') v ((a ->2 b) ^ (a ->2 c)))
26 le1 146 . . . . . . 7 ((b' ^ c') v ((a ->2 b) ^ (a ->2 c))) =< 1
2725, 26lebi 145 . . . . . 6 1 = ((b' ^ c') v ((a ->2 b) ^ (a ->2 c)))
2810u2lemle2 716 . . . . . . . . 9 a =< b
2928lecon 154 . . . . . . . 8 b' =< a'
3029leran 153 . . . . . . 7 (b' ^ c') =< (a' ^ c')
3130leror 152 . . . . . 6 ((b' ^ c') v ((a ->2 b) ^ (a ->2 c))) =< ((a' ^ c') v ((a ->2 b) ^ (a ->2 c)))
3227, 31bltr 138 . . . . 5 1 =< ((a' ^ c') v ((a ->2 b) ^ (a ->2 c)))
3318, 32lebi 145 . . . 4 ((a' ^ c') v ((a ->2 b) ^ (a ->2 c))) = 1
3417, 33ax-r2 36 . . 3 ((a' ^ c') v (c v (a' ^ c'))) = 1
352, 4, 343tr2 64 . 2 (c v (a' ^ c')) = 1
361, 35ax-r2 36 1 (a ->2 c) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  1wt 8   ->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: (None)
  Copyright terms: Public domain W3C validator