QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  bi4 Unicode version
Theorem bi4 840
Description: Chained biconditional.
Assertion
Ref Expression
bi4 (((a == b) ^ (b == c)) ^ (c == d)) = ((((a ^ b) ^ c) ^ d) v (((a' ^ b') ^ c') ^ d'))
Proof of Theorem bi4
StepHypRef Expression
1 bi3 839 . . 3 ((a == b) ^ (b == c)) = (((a ^ b) ^ c) v ((a' ^ b') ^ c'))
2 u12lembi 726 . . . 4 ((c ->1 d) ^ (d ->2 c)) = (c == d)
32ax-r1 35 . . 3 (c == d) = ((c ->1 d) ^ (d ->2 c))
41, 32an 79 . 2 (((a == b) ^ (b == c)) ^ (c == d)) = ((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ ((c ->1 d) ^ (d ->2 c)))
5 df-i1 44 . . . . . 6 (c ->1 d) = (c' v (c ^ d))
65lan 77 . . . . 5 ((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ (c ->1 d)) = ((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ (c' v (c ^ d)))
7 leao2 163 . . . . . . 7 ((a' ^ b') ^ c') =< (c' v (c ^ d))
87lecom 180 . . . . . 6 ((a' ^ b') ^ c') C (c' v (c ^ d))
9 leao4 165 . . . . . . . . . 10 ((a ^ b) ^ c) =< ((a' ^ b')' v c)
10 oran2 92 . . . . . . . . . 10 ((a' ^ b')' v c) = ((a' ^ b') ^ c')'
119, 10lbtr 139 . . . . . . . . 9 ((a ^ b) ^ c) =< ((a' ^ b') ^ c')'
1211lecom 180 . . . . . . . 8 ((a ^ b) ^ c) C ((a' ^ b') ^ c')'
1312comcom 453 . . . . . . 7 ((a' ^ b') ^ c')' C ((a ^ b) ^ c)
1413comcom6 459 . . . . . 6 ((a' ^ b') ^ c') C ((a ^ b) ^ c)
158, 14fh2rc 480 . . . . 5 ((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ (c' v (c ^ d))) = ((((a ^ b) ^ c) ^ (c' v (c ^ d))) v (((a' ^ b') ^ c') ^ (c' v (c ^ d))))
16 comanr2 465 . . . . . . . . 9 c C ((a ^ b) ^ c)
1716comcom3 454 . . . . . . . 8 c' C ((a ^ b) ^ c)
18 comanr1 464 . . . . . . . . 9 c C (c ^ d)
1918comcom3 454 . . . . . . . 8 c' C (c ^ d)
2017, 19fh2 470 . . . . . . 7 (((a ^ b) ^ c) ^ (c' v (c ^ d))) = ((((a ^ b) ^ c) ^ c') v (((a ^ b) ^ c) ^ (c ^ d)))
21 anass 76 . . . . . . . . 9 (((a ^ b) ^ c) ^ c') = ((a ^ b) ^ (c ^ c'))
22 dff 101 . . . . . . . . . . 11 0 = (c ^ c')
2322lan 77 . . . . . . . . . 10 ((a ^ b) ^ 0) = ((a ^ b) ^ (c ^ c'))
2423ax-r1 35 . . . . . . . . 9 ((a ^ b) ^ (c ^ c')) = ((a ^ b) ^ 0)
25 an0 108 . . . . . . . . 9 ((a ^ b) ^ 0) = 0
2621, 24, 253tr 65 . . . . . . . 8 (((a ^ b) ^ c) ^ c') = 0
27 anass 76 . . . . . . . . . 10 ((((a ^ b) ^ c) ^ c) ^ d) = (((a ^ b) ^ c) ^ (c ^ d))
2827ax-r1 35 . . . . . . . . 9 (((a ^ b) ^ c) ^ (c ^ d)) = ((((a ^ b) ^ c) ^ c) ^ d)
29 anass 76 . . . . . . . . . . 11 (((a ^ b) ^ c) ^ c) = ((a ^ b) ^ (c ^ c))
30 anidm 111 . . . . . . . . . . . 12 (c ^ c) = c
3130lan 77 . . . . . . . . . . 11 ((a ^ b) ^ (c ^ c)) = ((a ^ b) ^ c)
3229, 31ax-r2 36 . . . . . . . . . 10 (((a ^ b) ^ c) ^ c) = ((a ^ b) ^ c)
3332ran 78 . . . . . . . . 9 ((((a ^ b) ^ c) ^ c) ^ d) = (((a ^ b) ^ c) ^ d)
3428, 33ax-r2 36 . . . . . . . 8 (((a ^ b) ^ c) ^ (c ^ d)) = (((a ^ b) ^ c) ^ d)
3526, 342or 72 . . . . . . 7 ((((a ^ b) ^ c) ^ c') v (((a ^ b) ^ c) ^ (c ^ d))) = (0 v (((a ^ b) ^ c) ^ d))
36 or0r 103 . . . . . . 7 (0 v (((a ^ b) ^ c) ^ d)) = (((a ^ b) ^ c) ^ d)
3720, 35, 363tr 65 . . . . . 6 (((a ^ b) ^ c) ^ (c' v (c ^ d))) = (((a ^ b) ^ c) ^ d)
38 comanr2 465 . . . . . . . 8 c' C ((a' ^ b') ^ c')
3938, 19fh2 470 . . . . . . 7 (((a' ^ b') ^ c') ^ (c' v (c ^ d))) = ((((a' ^ b') ^ c') ^ c') v (((a' ^ b') ^ c') ^ (c ^ d)))
40 anass 76 . . . . . . . . 9 (((a' ^ b') ^ c') ^ c') = ((a' ^ b') ^ (c' ^ c'))
41 anidm 111 . . . . . . . . . 10 (c' ^ c') = c'
4241lan 77 . . . . . . . . 9 ((a' ^ b') ^ (c' ^ c')) = ((a' ^ b') ^ c')
4340, 42ax-r2 36 . . . . . . . 8 (((a' ^ b') ^ c') ^ c') = ((a' ^ b') ^ c')
44 an4 86 . . . . . . . . 9 (((a' ^ b') ^ c') ^ (c ^ d)) = (((a' ^ b') ^ c) ^ (c' ^ d))
45 anass 76 . . . . . . . . 9 (((a' ^ b') ^ c) ^ (c' ^ d)) = ((a' ^ b') ^ (c ^ (c' ^ d)))
4622ran 78 . . . . . . . . . . . . 13 (0 ^ d) = ((c ^ c') ^ d)
4746ax-r1 35 . . . . . . . . . . . 12 ((c ^ c') ^ d) = (0 ^ d)
48 anass 76 . . . . . . . . . . . 12 ((c ^ c') ^ d) = (c ^ (c' ^ d))
49 an0r 109 . . . . . . . . . . . 12 (0 ^ d) = 0
5047, 48, 493tr2 64 . . . . . . . . . . 11 (c ^ (c' ^ d)) = 0
5150lan 77 . . . . . . . . . 10 ((a' ^ b') ^ (c ^ (c' ^ d))) = ((a' ^ b') ^ 0)
52 an0 108 . . . . . . . . . 10 ((a' ^ b') ^ 0) = 0
5351, 52ax-r2 36 . . . . . . . . 9 ((a' ^ b') ^ (c ^ (c' ^ d))) = 0
5444, 45, 533tr 65 . . . . . . . 8 (((a' ^ b') ^ c') ^ (c ^ d)) = 0
5543, 542or 72 . . . . . . 7 ((((a' ^ b') ^ c') ^ c') v (((a' ^ b') ^ c') ^ (c ^ d))) = (((a' ^ b') ^ c') v 0)
56 or0 102 . . . . . . 7 (((a' ^ b') ^ c') v 0) = ((a' ^ b') ^ c')
5739, 55, 563tr 65 . . . . . 6 (((a' ^ b') ^ c') ^ (c' v (c ^ d))) = ((a' ^ b') ^ c')
5837, 572or 72 . . . . 5 ((((a ^ b) ^ c) ^ (c' v (c ^ d))) v (((a' ^ b') ^ c') ^ (c' v (c ^ d)))) = ((((a ^ b) ^ c) ^ d) v ((a' ^ b') ^ c'))
596, 15, 583tr 65 . . . 4 ((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ (c ->1 d)) = ((((a ^ b) ^ c) ^ d) v ((a' ^ b') ^ c'))
6059ran 78 . . 3 (((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ (c ->1 d)) ^ (d ->2 c)) = (((((a ^ b) ^ c) ^ d) v ((a' ^ b') ^ c')) ^ (d ->2 c))
61 anass 76 . . 3 (((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ (c ->1 d)) ^ (d ->2 c)) = ((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ ((c ->1 d) ^ (d ->2 c)))
62 anass 76 . . . . . . . 8 ((((a ^ b) ^ c) ^ d) ^ (d ->2 c)) = (((a ^ b) ^ c) ^ (d ^ (d ->2 c)))
63 an4 86 . . . . . . . 8 (((a ^ b) ^ c) ^ (d ^ (d ->2 c))) = (((a ^ b) ^ d) ^ (c ^ (d ->2 c)))
64 ancom 74 . . . . . . . . . . 11 (c ^ (d ->2 c)) = ((d ->2 c) ^ c)
65 u2lemab 611 . . . . . . . . . . 11 ((d ->2 c) ^ c) = c
6664, 65ax-r2 36 . . . . . . . . . 10 (c ^ (d ->2 c)) = c
6766lan 77 . . . . . . . . 9 (((a ^ b) ^ d) ^ (c ^ (d ->2 c))) = (((a ^ b) ^ d) ^ c)
68 an32 83 . . . . . . . . 9 (((a ^ b) ^ d) ^ c) = (((a ^ b) ^ c) ^ d)
6967, 68ax-r2 36 . . . . . . . 8 (((a ^ b) ^ d) ^ (c ^ (d ->2 c))) = (((a ^ b) ^ c) ^ d)
7062, 63, 693tr 65 . . . . . . 7 ((((a ^ b) ^ c) ^ d) ^ (d ->2 c)) = (((a ^ b) ^ c) ^ d)
7170df2le1 135 . . . . . 6 (((a ^ b) ^ c) ^ d) =< (d ->2 c)
7271lecom 180 . . . . 5 (((a ^ b) ^ c) ^ d) C (d ->2 c)
73 an32 83 . . . . . . . . 9 (((a ^ b) ^ c) ^ d) = (((a ^ b) ^ d) ^ c)
74 leao4 165 . . . . . . . . 9 (((a ^ b) ^ d) ^ c) =< ((a' ^ b')' v c)
7573, 74bltr 138 . . . . . . . 8 (((a ^ b) ^ c) ^ d) =< ((a' ^ b')' v c)
7675, 10lbtr 139 . . . . . . 7 (((a ^ b) ^ c) ^ d) =< ((a' ^ b') ^ c')'
7776lecom 180 . . . . . 6 (((a ^ b) ^ c) ^ d) C ((a' ^ b') ^ c')'
7877comcom7 460 . . . . 5 (((a ^ b) ^ c) ^ d) C ((a' ^ b') ^ c')
7972, 78fh2r 474 . . . 4 (((((a ^ b) ^ c) ^ d) v ((a' ^ b') ^ c')) ^ (d ->2 c)) = (((((a ^ b) ^ c) ^ d) ^ (d ->2 c)) v (((a' ^ b') ^ c') ^ (d ->2 c)))
80 anass 76 . . . . . 6 (((a' ^ b') ^ c') ^ (d ->2 c)) = ((a' ^ b') ^ (c' ^ (d ->2 c)))
81 ancom 74 . . . . . . . 8 (c' ^ (d ->2 c)) = ((d ->2 c) ^ c')
82 u2lemanb 616 . . . . . . . 8 ((d ->2 c) ^ c') = (d' ^ c')
8381, 82ax-r2 36 . . . . . . 7 (c' ^ (d ->2 c)) = (d' ^ c')
8483lan 77 . . . . . 6 ((a' ^ b') ^ (c' ^ (d ->2 c))) = ((a' ^ b') ^ (d' ^ c'))
85 an12 81 . . . . . . 7 ((a' ^ b') ^ (d' ^ c')) = (d' ^ ((a' ^ b') ^ c'))
86 ancom 74 . . . . . . 7 (d' ^ ((a' ^ b') ^ c')) = (((a' ^ b') ^ c') ^ d')
8785, 86ax-r2 36 . . . . . 6 ((a' ^ b') ^ (d' ^ c')) = (((a' ^ b') ^ c') ^ d')
8880, 84, 873tr 65 . . . . 5 (((a' ^ b') ^ c') ^ (d ->2 c)) = (((a' ^ b') ^ c') ^ d')
8970, 882or 72 . . . 4 (((((a ^ b) ^ c) ^ d) ^ (d ->2 c)) v (((a' ^ b') ^ c') ^ (d ->2 c))) = ((((a ^ b) ^ c) ^ d) v (((a' ^ b') ^ c') ^ d'))
9079, 89ax-r2 36 . . 3 (((((a ^ b) ^ c) ^ d) v ((a' ^ b') ^ c')) ^ (d ->2 c)) = ((((a ^ b) ^ c) ^ d) v (((a' ^ b') ^ c') ^ d'))
9160, 61, 903tr2 64 . 2 ((((a ^ b) ^ c) v ((a' ^ b') ^ c')) ^ ((c ->1 d) ^ (d ->2 c))) = ((((a ^ b) ^ c) ^ d) v (((a' ^ b') ^ c') ^ d'))
924, 91ax-r2 36 1 (((a == b) ^ (b == c)) ^ (c == d)) = ((((a ^ b) ^ c) ^ d) v (((a' ^ b') ^ c') ^ d'))
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:  mhcor1  888
  Copyright terms: Public domain W3C validator