QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  cancellem Unicode version
Theorem cancellem 891
Description: Lemma for cancellation law eliminating ->1 consequent.
Hypothesis
Ref Expression
cancel.1 ((d v (a ->1 c)) ->1 c) = ((d v (b ->1 c)) ->1 c)
Assertion
Ref Expression
cancellem (d v (a ->1 c)) =< (d v (b ->1 c))
Proof of Theorem cancellem
StepHypRef Expression
1 i1abs 801 . . 3 (((d v (a ->1 c)) ->1 c)' v ((d v (a ->1 c)) ^ c)) = (d v (a ->1 c))
21ax-r1 35 . 2 (d v (a ->1 c)) = (((d v (a ->1 c)) ->1 c)' v ((d v (a ->1 c)) ^ c))
3 leo 158 . . . . 5 (d v (b ->1 c))' =< ((d v (b ->1 c))' v ((d v (b ->1 c)) ^ c))
4 cancel.1 . . . . . . 7 ((d v (a ->1 c)) ->1 c) = ((d v (b ->1 c)) ->1 c)
5 df-i1 44 . . . . . . 7 ((d v (b ->1 c)) ->1 c) = ((d v (b ->1 c))' v ((d v (b ->1 c)) ^ c))
64, 5ax-r2 36 . . . . . 6 ((d v (a ->1 c)) ->1 c) = ((d v (b ->1 c))' v ((d v (b ->1 c)) ^ c))
76ax-r1 35 . . . . 5 ((d v (b ->1 c))' v ((d v (b ->1 c)) ^ c)) = ((d v (a ->1 c)) ->1 c)
83, 7lbtr 139 . . . 4 (d v (b ->1 c))' =< ((d v (a ->1 c)) ->1 c)
98lecon2 156 . . 3 ((d v (a ->1 c)) ->1 c)' =< (d v (b ->1 c))
10 leor 159 . . . . . 6 ((d v (a ->1 c)) ^ c) =< ((d v (a ->1 c))' v ((d v (a ->1 c)) ^ c))
11 df-i1 44 . . . . . . . 8 ((d v (a ->1 c)) ->1 c) = ((d v (a ->1 c))' v ((d v (a ->1 c)) ^ c))
1211ax-r1 35 . . . . . . 7 ((d v (a ->1 c))' v ((d v (a ->1 c)) ^ c)) = ((d v (a ->1 c)) ->1 c)
1312, 4ax-r2 36 . . . . . 6 ((d v (a ->1 c))' v ((d v (a ->1 c)) ^ c)) = ((d v (b ->1 c)) ->1 c)
1410, 13lbtr 139 . . . . 5 ((d v (a ->1 c)) ^ c) =< ((d v (b ->1 c)) ->1 c)
15 lear 161 . . . . 5 ((d v (a ->1 c)) ^ c) =< c
1614, 15ler2an 173 . . . 4 ((d v (a ->1 c)) ^ c) =< (((d v (b ->1 c)) ->1 c) ^ c)
17 coman2 186 . . . . . . 7 ((d v (b ->1 c)) ^ c) C c
18 coman1 185 . . . . . . . 8 ((d v (b ->1 c)) ^ c) C (d v (b ->1 c))
1918comcom2 183 . . . . . . 7 ((d v (b ->1 c)) ^ c) C (d v (b ->1 c))'
2017, 19fh2rc 480 . . . . . 6 (((d v (b ->1 c))' v ((d v (b ->1 c)) ^ c)) ^ c) = (((d v (b ->1 c))' ^ c) v (((d v (b ->1 c)) ^ c) ^ c))
215ran 78 . . . . . 6 (((d v (b ->1 c)) ->1 c) ^ c) = (((d v (b ->1 c))' v ((d v (b ->1 c)) ^ c)) ^ c)
22 id 59 . . . . . 6 (((d v (b ->1 c))' ^ c) v (((d v (b ->1 c)) ^ c) ^ c)) = (((d v (b ->1 c))' ^ c) v (((d v (b ->1 c)) ^ c) ^ c))
2320, 21, 223tr1 63 . . . . 5 (((d v (b ->1 c)) ->1 c) ^ c) = (((d v (b ->1 c))' ^ c) v (((d v (b ->1 c)) ^ c) ^ c))
24 leao4 165 . . . . . . . 8 ((d' ^ (b ^ c)') ^ (b ^ c)) =< (b' v (b ^ c))
2524lerr 150 . . . . . . 7 ((d' ^ (b ^ c)') ^ (b ^ c)) =< (d v (b' v (b ^ c)))
26 df-i1 44 . . . . . . . . . . . 12 (b ->1 c) = (b' v (b ^ c))
2726lor 70 . . . . . . . . . . 11 (d v (b ->1 c)) = (d v (b' v (b ^ c)))
2827ax-r4 37 . . . . . . . . . 10 (d v (b ->1 c))' = (d v (b' v (b ^ c)))'
29 an12 81 . . . . . . . . . . . 12 (b ^ (d' ^ (b ^ c)')) = (d' ^ (b ^ (b ^ c)'))
30 anor1 88 . . . . . . . . . . . . 13 (b ^ (b ^ c)') = (b' v (b ^ c))'
3130lan 77 . . . . . . . . . . . 12 (d' ^ (b ^ (b ^ c)')) = (d' ^ (b' v (b ^ c))')
32 anor3 90 . . . . . . . . . . . 12 (d' ^ (b' v (b ^ c))') = (d v (b' v (b ^ c)))'
3329, 31, 323tr 65 . . . . . . . . . . 11 (b ^ (d' ^ (b ^ c)')) = (d v (b' v (b ^ c)))'
3433ax-r1 35 . . . . . . . . . 10 (d v (b' v (b ^ c)))' = (b ^ (d' ^ (b ^ c)'))
35 ancom 74 . . . . . . . . . 10 (b ^ (d' ^ (b ^ c)')) = ((d' ^ (b ^ c)') ^ b)
3628, 34, 353tr 65 . . . . . . . . 9 (d v (b ->1 c))' = ((d' ^ (b ^ c)') ^ b)
3736ran 78 . . . . . . . 8 ((d v (b ->1 c))' ^ c) = (((d' ^ (b ^ c)') ^ b) ^ c)
38 anass 76 . . . . . . . 8 (((d' ^ (b ^ c)') ^ b) ^ c) = ((d' ^ (b ^ c)') ^ (b ^ c))
3937, 38ax-r2 36 . . . . . . 7 ((d v (b ->1 c))' ^ c) = ((d' ^ (b ^ c)') ^ (b ^ c))
4025, 39, 27le3tr1 140 . . . . . 6 ((d v (b ->1 c))' ^ c) =< (d v (b ->1 c))
41 lea 160 . . . . . . 7 ((d v (b ->1 c)) ^ c) =< (d v (b ->1 c))
4241lel 151 . . . . . 6 (((d v (b ->1 c)) ^ c) ^ c) =< (d v (b ->1 c))
4340, 42lel2or 170 . . . . 5 (((d v (b ->1 c))' ^ c) v (((d v (b ->1 c)) ^ c) ^ c)) =< (d v (b ->1 c))
4423, 43bltr 138 . . . 4 (((d v (b ->1 c)) ->1 c) ^ c) =< (d v (b ->1 c))
4516, 44letr 137 . . 3 ((d v (a ->1 c)) ^ c) =< (d v (b ->1 c))
469, 45lel2or 170 . 2 (((d v (a ->1 c)) ->1 c)' v ((d v (a ->1 c)) ^ c)) =< (d v (b ->1 c))
472, 46bltr 138 1 (d v (a ->1 c)) =< (d v (b ->1 c))
Colors of variables: term
Syntax hints:   = wb 1   =< wle 2  'wn 4   v wo 6   ^ wa 7   ->1 wi1 12
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-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  cancel  892
  Copyright terms: Public domain W3C validator