QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  bi3 Unicode version
Theorem bi3 839
Description: Chained biconditional.
Assertion
Ref Expression
bi3 ((a == b) ^ (b == c)) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
Proof of Theorem bi3
StepHypRef Expression
1 dfb 94 . . 3 (a == b) = ((a ^ b) v (a' ^ b'))
2 u12lembi 726 . . . 4 ((b ->1 c) ^ (c ->2 b)) = (b == c)
32ax-r1 35 . . 3 (b == c) = ((b ->1 c) ^ (c ->2 b))
41, 32an 79 . 2 ((a == b) ^ (b == c)) = (((a ^ b) v (a' ^ b')) ^ ((b ->1 c) ^ (c ->2 b)))
5 df-i1 44 . . . . . 6 (b ->1 c) = (b' v (b ^ c))
65lan 77 . . . . 5 (((a ^ b) v (a' ^ b')) ^ (b ->1 c)) = (((a ^ b) v (a' ^ b')) ^ (b' v (b ^ c)))
7 lear 161 . . . . . . . 8 (a' ^ b') =< b'
8 leo 158 . . . . . . . 8 b' =< (b' v (b ^ c))
97, 8letr 137 . . . . . . 7 (a' ^ b') =< (b' v (b ^ c))
109lecom 180 . . . . . 6 (a' ^ b') C (b' v (b ^ c))
11 coman1 185 . . . . . . . 8 (a' ^ b') C a'
1211comcom7 460 . . . . . . 7 (a' ^ b') C a
13 coman2 186 . . . . . . . 8 (a' ^ b') C b'
1413comcom7 460 . . . . . . 7 (a' ^ b') C b
1512, 14com2an 484 . . . . . 6 (a' ^ b') C (a ^ b)
1610, 15fh2rc 480 . . . . 5 (((a ^ b) v (a' ^ b')) ^ (b' v (b ^ c))) = (((a ^ b) ^ (b' v (b ^ c))) v ((a' ^ b') ^ (b' v (b ^ c))))
17 comanr2 465 . . . . . . . . 9 b C (a ^ b)
1817comcom3 454 . . . . . . . 8 b' C (a ^ b)
19 comanr1 464 . . . . . . . . 9 b C (b ^ c)
2019comcom3 454 . . . . . . . 8 b' C (b ^ c)
2118, 20fh2 470 . . . . . . 7 ((a ^ b) ^ (b' v (b ^ c))) = (((a ^ b) ^ b') v ((a ^ b) ^ (b ^ c)))
22 anass 76 . . . . . . . . 9 ((a ^ b) ^ b') = (a ^ (b ^ b'))
23 dff 101 . . . . . . . . . . 11 0 = (b ^ b')
2423lan 77 . . . . . . . . . 10 (a ^ 0) = (a ^ (b ^ b'))
2524ax-r1 35 . . . . . . . . 9 (a ^ (b ^ b')) = (a ^ 0)
26 an0 108 . . . . . . . . 9 (a ^ 0) = 0
2722, 25, 263tr 65 . . . . . . . 8 ((a ^ b) ^ b') = 0
28 anass 76 . . . . . . . . . 10 (((a ^ b) ^ b) ^ c) = ((a ^ b) ^ (b ^ c))
2928ax-r1 35 . . . . . . . . 9 ((a ^ b) ^ (b ^ c)) = (((a ^ b) ^ b) ^ c)
30 anass 76 . . . . . . . . . . 11 ((a ^ b) ^ b) = (a ^ (b ^ b))
31 anidm 111 . . . . . . . . . . . 12 (b ^ b) = b
3231lan 77 . . . . . . . . . . 11 (a ^ (b ^ b)) = (a ^ b)
3330, 32ax-r2 36 . . . . . . . . . 10 ((a ^ b) ^ b) = (a ^ b)
3433ran 78 . . . . . . . . 9 (((a ^ b) ^ b) ^ c) = ((a ^ b) ^ c)
3529, 34ax-r2 36 . . . . . . . 8 ((a ^ b) ^ (b ^ c)) = ((a ^ b) ^ c)
3627, 352or 72 . . . . . . 7 (((a ^ b) ^ b') v ((a ^ b) ^ (b ^ c))) = (0 v ((a ^ b) ^ c))
37 or0r 103 . . . . . . 7 (0 v ((a ^ b) ^ c)) = ((a ^ b) ^ c)
3821, 36, 373tr 65 . . . . . 6 ((a ^ b) ^ (b' v (b ^ c))) = ((a ^ b) ^ c)
3913comcom 453 . . . . . . . 8 b' C (a' ^ b')
4039, 20fh2 470 . . . . . . 7 ((a' ^ b') ^ (b' v (b ^ c))) = (((a' ^ b') ^ b') v ((a' ^ b') ^ (b ^ c)))
41 anass 76 . . . . . . . . 9 ((a' ^ b') ^ b') = (a' ^ (b' ^ b'))
42 anidm 111 . . . . . . . . . 10 (b' ^ b') = b'
4342lan 77 . . . . . . . . 9 (a' ^ (b' ^ b')) = (a' ^ b')
4441, 43ax-r2 36 . . . . . . . 8 ((a' ^ b') ^ b') = (a' ^ b')
45 an4 86 . . . . . . . . 9 ((a' ^ b') ^ (b ^ c)) = ((a' ^ b) ^ (b' ^ c))
46 anass 76 . . . . . . . . 9 ((a' ^ b) ^ (b' ^ c)) = (a' ^ (b ^ (b' ^ c)))
4723ran 78 . . . . . . . . . . . . 13 (0 ^ c) = ((b ^ b') ^ c)
4847ax-r1 35 . . . . . . . . . . . 12 ((b ^ b') ^ c) = (0 ^ c)
49 anass 76 . . . . . . . . . . . 12 ((b ^ b') ^ c) = (b ^ (b' ^ c))
50 an0r 109 . . . . . . . . . . . 12 (0 ^ c) = 0
5148, 49, 503tr2 64 . . . . . . . . . . 11 (b ^ (b' ^ c)) = 0
5251lan 77 . . . . . . . . . 10 (a' ^ (b ^ (b' ^ c))) = (a' ^ 0)
53 an0 108 . . . . . . . . . 10 (a' ^ 0) = 0
5452, 53ax-r2 36 . . . . . . . . 9 (a' ^ (b ^ (b' ^ c))) = 0
5545, 46, 543tr 65 . . . . . . . 8 ((a' ^ b') ^ (b ^ c)) = 0
5644, 552or 72 . . . . . . 7 (((a' ^ b') ^ b') v ((a' ^ b') ^ (b ^ c))) = ((a' ^ b') v 0)
57 or0 102 . . . . . . 7 ((a' ^ b') v 0) = (a' ^ b')
5840, 56, 573tr 65 . . . . . 6 ((a' ^ b') ^ (b' v (b ^ c))) = (a' ^ b')
5938, 582or 72 . . . . 5 (((a ^ b) ^ (b' v (b ^ c))) v ((a' ^ b') ^ (b' v (b ^ c)))) = (((a ^ b) ^ c) v (a' ^ b'))
606, 16, 593tr 65 . . . 4 (((a ^ b) v (a' ^ b')) ^ (b ->1 c)) = (((a ^ b) ^ c) v (a' ^ b'))
6160ran 78 . . 3 ((((a ^ b) v (a' ^ b')) ^ (b ->1 c)) ^ (c ->2 b)) = ((((a ^ b) ^ c) v (a' ^ b')) ^ (c ->2 b))
62 anass 76 . . 3 ((((a ^ b) v (a' ^ b')) ^ (b ->1 c)) ^ (c ->2 b)) = (((a ^ b) v (a' ^ b')) ^ ((b ->1 c) ^ (c ->2 b)))
63 lear 161 . . . . . . . 8 ((a ^ c) ^ b) =< b
64 leo 158 . . . . . . . 8 b =< (b v (c' ^ b'))
6563, 64letr 137 . . . . . . 7 ((a ^ c) ^ b) =< (b v (c' ^ b'))
66 an32 83 . . . . . . 7 ((a ^ b) ^ c) = ((a ^ c) ^ b)
67 df-i2 45 . . . . . . 7 (c ->2 b) = (b v (c' ^ b'))
6865, 66, 67le3tr1 140 . . . . . 6 ((a ^ b) ^ c) =< (c ->2 b)
6968lecom 180 . . . . 5 ((a ^ b) ^ c) C (c ->2 b)
70 anass 76 . . . . . . . . . 10 ((a ^ b) ^ c) = (a ^ (b ^ c))
71 lea 160 . . . . . . . . . 10 (a ^ (b ^ c)) =< a
7270, 71bltr 138 . . . . . . . . 9 ((a ^ b) ^ c) =< a
73 leo 158 . . . . . . . . 9 a =< (a v b)
7472, 73letr 137 . . . . . . . 8 ((a ^ b) ^ c) =< (a v b)
75 oran 87 . . . . . . . 8 (a v b) = (a' ^ b')'
7674, 75lbtr 139 . . . . . . 7 ((a ^ b) ^ c) =< (a' ^ b')'
7776lecom 180 . . . . . 6 ((a ^ b) ^ c) C (a' ^ b')'
7877comcom7 460 . . . . 5 ((a ^ b) ^ c) C (a' ^ b')
7969, 78fh2r 474 . . . 4 ((((a ^ b) ^ c) v (a' ^ b')) ^ (c ->2 b)) = ((((a ^ b) ^ c) ^ (c ->2 b)) v ((a' ^ b') ^ (c ->2 b)))
80 anass 76 . . . . . 6 (((a ^ b) ^ c) ^ (c ->2 b)) = ((a ^ b) ^ (c ^ (c ->2 b)))
81 an4 86 . . . . . 6 ((a ^ b) ^ (c ^ (c ->2 b))) = ((a ^ c) ^ (b ^ (c ->2 b)))
82 ancom 74 . . . . . . . . 9 (b ^ (c ->2 b)) = ((c ->2 b) ^ b)
83 u2lemab 611 . . . . . . . . 9 ((c ->2 b) ^ b) = b
8482, 83ax-r2 36 . . . . . . . 8 (b ^ (c ->2 b)) = b
8584lan 77 . . . . . . 7 ((a ^ c) ^ (b ^ (c ->2 b))) = ((a ^ c) ^ b)
86 an32 83 . . . . . . 7 ((a ^ c) ^ b) = ((a ^ b) ^ c)
8785, 86ax-r2 36 . . . . . 6 ((a ^ c) ^ (b ^ (c ->2 b))) = ((a ^ b) ^ c)
8880, 81, 873tr 65 . . . . 5 (((a ^ b) ^ c) ^ (c ->2 b)) = ((a ^ b) ^ c)
89 anass 76 . . . . . 6 ((a' ^ b') ^ (c ->2 b)) = (a' ^ (b' ^ (c ->2 b)))
90 ancom 74 . . . . . . . 8 (b' ^ (c ->2 b)) = ((c ->2 b) ^ b')
91 u2lemanb 616 . . . . . . . 8 ((c ->2 b) ^ b') = (c' ^ b')
9290, 91ax-r2 36 . . . . . . 7 (b' ^ (c ->2 b)) = (c' ^ b')
9392lan 77 . . . . . 6 (a' ^ (b' ^ (c ->2 b))) = (a' ^ (c' ^ b'))
94 an12 81 . . . . . . 7 (a' ^ (c' ^ b')) = (c' ^ (a' ^ b'))
95 ancom 74 . . . . . . 7 (c' ^ (a' ^ b')) = ((a' ^ b') ^ c')
9694, 95ax-r2 36 . . . . . 6 (a' ^ (c' ^ b')) = ((a' ^ b') ^ c')
9789, 93, 963tr 65 . . . . 5 ((a' ^ b') ^ (c ->2 b)) = ((a' ^ b') ^ c')
9888, 972or 72 . . . 4 ((((a ^ b) ^ c) ^ (c ->2 b)) v ((a' ^ b') ^ (c ->2 b))) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
9979, 98ax-r2 36 . . 3 ((((a ^ b) ^ c) v (a' ^ b')) ^ (c ->2 b)) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
10061, 62, 993tr2 64 . 2 (((a ^ b) v (a' ^ b')) ^ ((b ->1 c) ^ (c ->2 b))) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
1014, 100ax-r2 36 1 ((a == b) ^ (b == c)) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  0wf 9   ->1 wi1 12   ->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-i1 44  df-i2 45  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  bi4  840  mlaconj4  844
  Copyright terms: Public domain W3C validator