QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  orbi Unicode version
Theorem orbi 842
Description: Disjunction of biconditionals.
Assertion
Ref Expression
orbi ((a == c) v (b == c)) = (((a ->2 c) v (b ->2 c)) ^ ((c ->1 a) v (c ->1 b)))
Proof of Theorem orbi
StepHypRef Expression
1 dfb 94 . . 3 (a == c) = ((a ^ c) v (a' ^ c'))
2 dfb 94 . . 3 (b == c) = ((b ^ c) v (b' ^ c'))
31, 22or 72 . 2 ((a == c) v (b == c)) = (((a ^ c) v (a' ^ c')) v ((b ^ c) v (b' ^ c')))
4 ax-a2 31 . 2 (((a ^ c) v (a' ^ c')) v ((b ^ c) v (b' ^ c'))) = (((b ^ c) v (b' ^ c')) v ((a ^ c) v (a' ^ c')))
5 ax-a3 32 . . 3 (((b ^ c) v (b' ^ c')) v ((a ^ c) v (a' ^ c'))) = ((b ^ c) v ((b' ^ c') v ((a ^ c) v (a' ^ c'))))
6 ancom 74 . . . . . . . 8 (a ^ c) = (c ^ a)
76lor 70 . . . . . . 7 ((b' ^ c') v (a ^ c)) = ((b' ^ c') v (c ^ a))
8 imp3 841 . . . . . . . 8 ((b ->2 c) ^ (c ->1 a)) = ((b' ^ c') v (c ^ a))
98ax-r1 35 . . . . . . 7 ((b' ^ c') v (c ^ a)) = ((b ->2 c) ^ (c ->1 a))
107, 9ax-r2 36 . . . . . 6 ((b' ^ c') v (a ^ c)) = ((b ->2 c) ^ (c ->1 a))
1110ax-r5 38 . . . . 5 (((b' ^ c') v (a ^ c)) v (a' ^ c')) = (((b ->2 c) ^ (c ->1 a)) v (a' ^ c'))
12 ax-a3 32 . . . . 5 (((b' ^ c') v (a ^ c)) v (a' ^ c')) = ((b' ^ c') v ((a ^ c) v (a' ^ c')))
13 df-i1 44 . . . . . . . 8 (c ->1 a) = (c' v (c ^ a))
14 lear 161 . . . . . . . . . . 11 (a' ^ c') =< c'
15 leo 158 . . . . . . . . . . 11 c' =< (c' v (c ^ a))
1614, 15letr 137 . . . . . . . . . 10 (a' ^ c') =< (c' v (c ^ a))
1716lecom 180 . . . . . . . . 9 (a' ^ c') C (c' v (c ^ a))
1817comcom 453 . . . . . . . 8 (c' v (c ^ a)) C (a' ^ c')
1913, 18bctr 181 . . . . . . 7 (c ->1 a) C (a' ^ c')
20 comi12 707 . . . . . . 7 (c ->1 a) C (b ->2 c)
2119, 20fh4rc 482 . . . . . 6 (((b ->2 c) ^ (c ->1 a)) v (a' ^ c')) = (((b ->2 c) v (a' ^ c')) ^ ((c ->1 a) v (a' ^ c')))
2213ax-r5 38 . . . . . . . 8 ((c ->1 a) v (a' ^ c')) = ((c' v (c ^ a)) v (a' ^ c'))
23 ax-a2 31 . . . . . . . 8 ((c' v (c ^ a)) v (a' ^ c')) = ((a' ^ c') v (c' v (c ^ a)))
2416df-le2 131 . . . . . . . 8 ((a' ^ c') v (c' v (c ^ a))) = (c' v (c ^ a))
2522, 23, 243tr 65 . . . . . . 7 ((c ->1 a) v (a' ^ c')) = (c' v (c ^ a))
2625lan 77 . . . . . 6 (((b ->2 c) v (a' ^ c')) ^ ((c ->1 a) v (a' ^ c'))) = (((b ->2 c) v (a' ^ c')) ^ (c' v (c ^ a)))
2721, 26ax-r2 36 . . . . 5 (((b ->2 c) ^ (c ->1 a)) v (a' ^ c')) = (((b ->2 c) v (a' ^ c')) ^ (c' v (c ^ a)))
2811, 12, 273tr2 64 . . . 4 ((b' ^ c') v ((a ^ c) v (a' ^ c'))) = (((b ->2 c) v (a' ^ c')) ^ (c' v (c ^ a)))
2928lor 70 . . 3 ((b ^ c) v ((b' ^ c') v ((a ^ c) v (a' ^ c')))) = ((b ^ c) v (((b ->2 c) v (a' ^ c')) ^ (c' v (c ^ a))))
30 df-i2 45 . . . . . . . 8 (b ->2 c) = (c v (b' ^ c'))
3130ax-r5 38 . . . . . . 7 ((b ->2 c) v (a' ^ c')) = ((c v (b' ^ c')) v (a' ^ c'))
32 ax-a3 32 . . . . . . 7 ((c v (b' ^ c')) v (a' ^ c')) = (c v ((b' ^ c') v (a' ^ c')))
3331, 32ax-r2 36 . . . . . 6 ((b ->2 c) v (a' ^ c')) = (c v ((b' ^ c') v (a' ^ c')))
34 lear 161 . . . . . . . . 9 (b ^ c) =< c
35 leo 158 . . . . . . . . 9 c =< (c v ((b' ^ c') v (a' ^ c')))
3634, 35letr 137 . . . . . . . 8 (b ^ c) =< (c v ((b' ^ c') v (a' ^ c')))
3736lecom 180 . . . . . . 7 (b ^ c) C (c v ((b' ^ c') v (a' ^ c')))
3837comcom 453 . . . . . 6 (c v ((b' ^ c') v (a' ^ c'))) C (b ^ c)
3933, 38bctr 181 . . . . 5 ((b ->2 c) v (a' ^ c')) C (b ^ c)
40 lea 160 . . . . . . . . . . 11 (c ^ (c ^ a)') =< c
4140, 35letr 137 . . . . . . . . . 10 (c ^ (c ^ a)') =< (c v ((b' ^ c') v (a' ^ c')))
4241lecom 180 . . . . . . . . 9 (c ^ (c ^ a)') C (c v ((b' ^ c') v (a' ^ c')))
4342comcom 453 . . . . . . . 8 (c v ((b' ^ c') v (a' ^ c'))) C (c ^ (c ^ a)')
44 anor1 88 . . . . . . . 8 (c ^ (c ^ a)') = (c' v (c ^ a))'
4543, 44cbtr 182 . . . . . . 7 (c v ((b' ^ c') v (a' ^ c'))) C (c' v (c ^ a))'
4645comcom7 460 . . . . . 6 (c v ((b' ^ c') v (a' ^ c'))) C (c' v (c ^ a))
4733, 46bctr 181 . . . . 5 ((b ->2 c) v (a' ^ c')) C (c' v (c ^ a))
4839, 47fh4 472 . . . 4 ((b ^ c) v (((b ->2 c) v (a' ^ c')) ^ (c' v (c ^ a)))) = (((b ^ c) v ((b ->2 c) v (a' ^ c'))) ^ ((b ^ c) v (c' v (c ^ a))))
4930lor 70 . . . . . . . 8 ((b ^ c) v (b ->2 c)) = ((b ^ c) v (c v (b' ^ c')))
50 leo 158 . . . . . . . . . 10 c =< (c v (b' ^ c'))
5134, 50letr 137 . . . . . . . . 9 (b ^ c) =< (c v (b' ^ c'))
5251df-le2 131 . . . . . . . 8 ((b ^ c) v (c v (b' ^ c'))) = (c v (b' ^ c'))
5349, 52ax-r2 36 . . . . . . 7 ((b ^ c) v (b ->2 c)) = (c v (b' ^ c'))
5453ax-r5 38 . . . . . 6 (((b ^ c) v (b ->2 c)) v (a' ^ c')) = ((c v (b' ^ c')) v (a' ^ c'))
55 ax-a3 32 . . . . . 6 (((b ^ c) v (b ->2 c)) v (a' ^ c')) = ((b ^ c) v ((b ->2 c) v (a' ^ c')))
56 ax-a2 31 . . . . . . . 8 ((c v (b' ^ c')) v (c v (a' ^ c'))) = ((c v (a' ^ c')) v (c v (b' ^ c')))
57 orordi 112 . . . . . . . 8 (c v ((b' ^ c') v (a' ^ c'))) = ((c v (b' ^ c')) v (c v (a' ^ c')))
58 df-i2 45 . . . . . . . . 9 (a ->2 c) = (c v (a' ^ c'))
5958, 302or 72 . . . . . . . 8 ((a ->2 c) v (b ->2 c)) = ((c v (a' ^ c')) v (c v (b' ^ c')))
6056, 57, 593tr1 63 . . . . . . 7 (c v ((b' ^ c') v (a' ^ c'))) = ((a ->2 c) v (b ->2 c))
6132, 60ax-r2 36 . . . . . 6 ((c v (b' ^ c')) v (a' ^ c')) = ((a ->2 c) v (b ->2 c))
6254, 55, 613tr2 64 . . . . 5 ((b ^ c) v ((b ->2 c) v (a' ^ c'))) = ((a ->2 c) v (b ->2 c))
63 or12 80 . . . . . 6 ((b ^ c) v (c' v (c ^ a))) = (c' v ((b ^ c) v (c ^ a)))
64 ax-a2 31 . . . . . . 7 ((c' v (b ^ c)) v (c' v (c ^ a))) = ((c' v (c ^ a)) v (c' v (b ^ c)))
65 orordi 112 . . . . . . 7 (c' v ((b ^ c) v (c ^ a))) = ((c' v (b ^ c)) v (c' v (c ^ a)))
66 df-i1 44 . . . . . . . . 9 (c ->1 b) = (c' v (c ^ b))
67 ancom 74 . . . . . . . . . 10 (c ^ b) = (b ^ c)
6867lor 70 . . . . . . . . 9 (c' v (c ^ b)) = (c' v (b ^ c))
6966, 68ax-r2 36 . . . . . . . 8 (c ->1 b) = (c' v (b ^ c))
7013, 692or 72 . . . . . . 7 ((c ->1 a) v (c ->1 b)) = ((c' v (c ^ a)) v (c' v (b ^ c)))
7164, 65, 703tr1 63 . . . . . 6 (c' v ((b ^ c) v (c ^ a))) = ((c ->1 a) v (c ->1 b))
7263, 71ax-r2 36 . . . . 5 ((b ^ c) v (c' v (c ^ a))) = ((c ->1 a) v (c ->1 b))
7362, 722an 79 . . . 4 (((b ^ c) v ((b ->2 c) v (a' ^ c'))) ^ ((b ^ c) v (c' v (c ^ a)))) = (((a ->2 c) v (b ->2 c)) ^ ((c ->1 a) v (c ->1 b)))
7448, 73ax-r2 36 . . 3 ((b ^ c) v (((b ->2 c) v (a' ^ c')) ^ (c' v (c ^ a)))) = (((a ->2 c) v (b ->2 c)) ^ ((c ->1 a) v (c ->1 b)))
755, 29, 743tr 65 . 2 (((b ^ c) v (b' ^ c')) v ((a ^ c) v (a' ^ c'))) = (((a ->2 c) v (b ->2 c)) ^ ((c ->1 a) v (c ->1 b)))
763, 4, 753tr 65 1 ((a == c) v (b == c)) = (((a ->2 c) v (b ->2 c)) ^ ((c ->1 a) v (c ->1 b)))
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7   ->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:  orbile  843
  Copyright terms: Public domain W3C validator