QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  neg3antlem2 Unicode version
Theorem neg3antlem2 865
Description: Lemma for negated antecedent identity.
Hypothesis
Ref Expression
neg3ant.1 (a ->3 c) = (b ->3 c)
Assertion
Ref Expression
neg3antlem2 a' =< (b ->1 c)
Proof of Theorem neg3antlem2
StepHypRef Expression
1 leor 159 . . . . 5 (a' ^ c) =< ((a ^ c) v (a' ^ c))
2 neg3ant.1 . . . . . . 7 (a ->3 c) = (b ->3 c)
32ran 78 . . . . . 6 ((a ->3 c) ^ c) = ((b ->3 c) ^ c)
4 u3lemab 612 . . . . . 6 ((a ->3 c) ^ c) = ((a ^ c) v (a' ^ c))
5 u3lemab 612 . . . . . 6 ((b ->3 c) ^ c) = ((b ^ c) v (b' ^ c))
63, 4, 53tr2 64 . . . . 5 ((a ^ c) v (a' ^ c)) = ((b ^ c) v (b' ^ c))
71, 6lbtr 139 . . . 4 (a' ^ c) =< ((b ^ c) v (b' ^ c))
8 leor 159 . . . . 5 (b ^ c) =< (b' v (b ^ c))
9 leao1 162 . . . . 5 (b' ^ c) =< (b' v (b ^ c))
108, 9lel2or 170 . . . 4 ((b ^ c) v (b' ^ c)) =< (b' v (b ^ c))
117, 10letr 137 . . 3 (a' ^ c) =< (b' v (b ^ c))
12 leor 159 . . . . . . . . . . . 12 (b ^ (b' v c)) =< (((b' ^ c) v (b' ^ c')) v (b ^ (b' v c)))
13 df-i3 46 . . . . . . . . . . . . . 14 (b ->3 c) = (((b' ^ c) v (b' ^ c')) v (b ^ (b' v c)))
142, 13ax-r2 36 . . . . . . . . . . . . 13 (a ->3 c) = (((b' ^ c) v (b' ^ c')) v (b ^ (b' v c)))
1514ax-r1 35 . . . . . . . . . . . 12 (((b' ^ c) v (b' ^ c')) v (b ^ (b' v c))) = (a ->3 c)
1612, 15lbtr 139 . . . . . . . . . . 11 (b ^ (b' v c)) =< (a ->3 c)
17 leao1 162 . . . . . . . . . . . 12 (b ^ (b' v c)) =< (b v c)
182ran 78 . . . . . . . . . . . . . . . 16 ((a ->3 c) ^ c') = ((b ->3 c) ^ c')
19 u3lemanb 617 . . . . . . . . . . . . . . . 16 ((a ->3 c) ^ c') = (a' ^ c')
20 u3lemanb 617 . . . . . . . . . . . . . . . 16 ((b ->3 c) ^ c') = (b' ^ c')
2118, 19, 203tr2 64 . . . . . . . . . . . . . . 15 (a' ^ c') = (b' ^ c')
22 anor3 90 . . . . . . . . . . . . . . 15 (a' ^ c') = (a v c)'
23 anor3 90 . . . . . . . . . . . . . . 15 (b' ^ c') = (b v c)'
2421, 22, 233tr2 64 . . . . . . . . . . . . . 14 (a v c)' = (b v c)'
2524con1 66 . . . . . . . . . . . . 13 (a v c) = (b v c)
2625ax-r1 35 . . . . . . . . . . . 12 (b v c) = (a v c)
2717, 26lbtr 139 . . . . . . . . . . 11 (b ^ (b' v c)) =< (a v c)
2816, 27ler2an 173 . . . . . . . . . 10 (b ^ (b' v c)) =< ((a ->3 c) ^ (a v c))
29 u3lem15 795 . . . . . . . . . 10 ((a ->3 c) ^ (a v c)) = ((a' v c) ^ (a v (a' ^ c)))
3028, 29lbtr 139 . . . . . . . . 9 (b ^ (b' v c)) =< ((a' v c) ^ (a v (a' ^ c)))
31 lear 161 . . . . . . . . 9 ((a' v c) ^ (a v (a' ^ c))) =< (a v (a' ^ c))
3230, 31letr 137 . . . . . . . 8 (b ^ (b' v c)) =< (a v (a' ^ c))
33 oran2 92 . . . . . . . . . 10 (b' v c) = (b ^ c')'
3433lan 77 . . . . . . . . 9 (b ^ (b' v c)) = (b ^ (b ^ c')')
35 anor1 88 . . . . . . . . 9 (b ^ (b ^ c')') = (b' v (b ^ c'))'
3634, 35ax-r2 36 . . . . . . . 8 (b ^ (b' v c)) = (b' v (b ^ c'))'
37 anor2 89 . . . . . . . . . 10 (a' ^ c) = (a v c')'
3837lor 70 . . . . . . . . 9 (a v (a' ^ c)) = (a v (a v c')')
39 oran1 91 . . . . . . . . 9 (a v (a v c')') = (a' ^ (a v c'))'
4038, 39ax-r2 36 . . . . . . . 8 (a v (a' ^ c)) = (a' ^ (a v c'))'
4132, 36, 40le3tr2 141 . . . . . . 7 (b' v (b ^ c'))' =< (a' ^ (a v c'))'
4241lecon1 155 . . . . . 6 (a' ^ (a v c')) =< (b' v (b ^ c'))
43 leo 158 . . . . . . . 8 a' =< (a' v c)
442ax-r5 38 . . . . . . . . 9 ((a ->3 c) v c) = ((b ->3 c) v c)
45 u3lemob 632 . . . . . . . . 9 ((a ->3 c) v c) = (a' v c)
46 u3lemob 632 . . . . . . . . 9 ((b ->3 c) v c) = (b' v c)
4744, 45, 463tr2 64 . . . . . . . 8 (a' v c) = (b' v c)
4843, 47lbtr 139 . . . . . . 7 a' =< (b' v c)
4948lel 151 . . . . . 6 (a' ^ (a v c')) =< (b' v c)
5042, 49ler2an 173 . . . . 5 (a' ^ (a v c')) =< ((b' v (b ^ c')) ^ (b' v c))
51 comor1 461 . . . . . . 7 (b' v c) C b'
5251comcom7 460 . . . . . . . 8 (b' v c) C b
53 comor2 462 . . . . . . . . 9 (b' v c) C c
5453comcom2 183 . . . . . . . 8 (b' v c) C c'
5552, 54com2an 484 . . . . . . 7 (b' v c) C (b ^ c')
5651, 55fh1r 473 . . . . . 6 ((b' v (b ^ c')) ^ (b' v c)) = ((b' ^ (b' v c)) v ((b ^ c') ^ (b' v c)))
57 anabs 121 . . . . . . 7 (b' ^ (b' v c)) = b'
5833lan 77 . . . . . . . 8 ((b ^ c') ^ (b' v c)) = ((b ^ c') ^ (b ^ c')')
59 dff 101 . . . . . . . . 9 0 = ((b ^ c') ^ (b ^ c')')
6059ax-r1 35 . . . . . . . 8 ((b ^ c') ^ (b ^ c')') = 0
6158, 60ax-r2 36 . . . . . . 7 ((b ^ c') ^ (b' v c)) = 0
6257, 612or 72 . . . . . 6 ((b' ^ (b' v c)) v ((b ^ c') ^ (b' v c))) = (b' v 0)
63 or0 102 . . . . . 6 (b' v 0) = b'
6456, 62, 633tr 65 . . . . 5 ((b' v (b ^ c')) ^ (b' v c)) = b'
6550, 64lbtr 139 . . . 4 (a' ^ (a v c')) =< b'
6665ler 149 . . 3 (a' ^ (a v c')) =< (b' v (b ^ c))
6711, 66lel2or 170 . 2 ((a' ^ c) v (a' ^ (a v c'))) =< (b' v (b ^ c))
68 id 59 . . . . 5 a' = a'
69 ax-a2 31 . . . . . 6 ((a' ^ c) v a') = (a' v (a' ^ c))
70 orabs 120 . . . . . 6 (a' v (a' ^ c)) = a'
7169, 70ax-r2 36 . . . . 5 ((a' ^ c) v a') = a'
7268, 68, 713tr1 63 . . . 4 a' = ((a' ^ c) v a')
73 df-t 41 . . . . 5 1 = ((a' ^ c) v (a' ^ c)')
74 oran1 91 . . . . . . 7 (a v c') = (a' ^ c)'
7574lor 70 . . . . . 6 ((a' ^ c) v (a v c')) = ((a' ^ c) v (a' ^ c)')
7675ax-r1 35 . . . . 5 ((a' ^ c) v (a' ^ c)') = ((a' ^ c) v (a v c'))
7773, 76ax-r2 36 . . . 4 1 = ((a' ^ c) v (a v c'))
7872, 772an 79 . . 3 (a' ^ 1) = (((a' ^ c) v a') ^ ((a' ^ c) v (a v c')))
79 an1 106 . . . 4 (a' ^ 1) = a'
8079ax-r1 35 . . 3 a' = (a' ^ 1)
81 coman1 185 . . . 4 (a' ^ c) C a'
8281comcom7 460 . . . . 5 (a' ^ c) C a
83 coman2 186 . . . . . 6 (a' ^ c) C c
8483comcom2 183 . . . . 5 (a' ^ c) C c'
8582, 84com2or 483 . . . 4 (a' ^ c) C (a v c')
8681, 85fh3 471 . . 3 ((a' ^ c) v (a' ^ (a v c'))) = (((a' ^ c) v a') ^ ((a' ^ c) v (a v c')))
8778, 80, 863tr1 63 . 2 a' = ((a' ^ c) v (a' ^ (a v c')))
88 df-i1 44 . 2 (b ->1 c) = (b' v (b ^ c))
8967, 87, 88le3tr1 140 1 a' =< (b ->1 c)
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6   ^ wa 7  1wt 8  0wf 9   ->1 wi1 12   ->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-r3 439
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  neg3ant1  866
  Copyright terms: Public domain W3C validator