QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  ud3lem1b Unicode version
Theorem ud3lem1b 567
Description: Lemma for unified disjunction.
Assertion
Ref Expression
ud3lem1b ((a ->3 b)' ^ (b ->3 a)') = 0
Proof of Theorem ud3lem1b
StepHypRef Expression
1 ud3lem0c 279 . . 3 (a ->3 b)' = (((a v b') ^ (a v b)) ^ (a' v (a ^ b')))
2 ud3lem0c 279 . . 3 (b ->3 a)' = (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))
31, 22an 79 . 2 ((a ->3 b)' ^ (b ->3 a)') = ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a'))))
4 an32 83 . . 3 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) = ((((a v b') ^ (a v b)) ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) ^ (a' v (a ^ b')))
5 an32 83 . . . . . 6 (((a v b') ^ (a v b)) ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) = (((a v b') ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) ^ (a v b))
6 an12 81 . . . . . . . . 9 ((a v b') ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) = (((b v a') ^ (b v a)) ^ ((a v b') ^ (b' v (b ^ a'))))
7 comor2 462 . . . . . . . . . . . . 13 (a v b') C b'
87comcom7 460 . . . . . . . . . . . . . 14 (a v b') C b
9 comor1 461 . . . . . . . . . . . . . . 15 (a v b') C a
109comcom2 183 . . . . . . . . . . . . . 14 (a v b') C a'
118, 10com2an 484 . . . . . . . . . . . . 13 (a v b') C (b ^ a')
127, 11fh1 469 . . . . . . . . . . . 12 ((a v b') ^ (b' v (b ^ a'))) = (((a v b') ^ b') v ((a v b') ^ (b ^ a')))
13 ancom 74 . . . . . . . . . . . . . . . 16 ((a v b') ^ b') = (b' ^ (a v b'))
14 ax-a2 31 . . . . . . . . . . . . . . . . 17 (a v b') = (b' v a)
1514lan 77 . . . . . . . . . . . . . . . 16 (b' ^ (a v b')) = (b' ^ (b' v a))
1613, 15ax-r2 36 . . . . . . . . . . . . . . 15 ((a v b') ^ b') = (b' ^ (b' v a))
17 anabs 121 . . . . . . . . . . . . . . 15 (b' ^ (b' v a)) = b'
1816, 17ax-r2 36 . . . . . . . . . . . . . 14 ((a v b') ^ b') = b'
19 anor1 88 . . . . . . . . . . . . . . . 16 (b ^ a') = (b' v a)'
2014, 192an 79 . . . . . . . . . . . . . . 15 ((a v b') ^ (b ^ a')) = ((b' v a) ^ (b' v a)')
21 dff 101 . . . . . . . . . . . . . . . 16 0 = ((b' v a) ^ (b' v a)')
2221ax-r1 35 . . . . . . . . . . . . . . 15 ((b' v a) ^ (b' v a)') = 0
2320, 22ax-r2 36 . . . . . . . . . . . . . 14 ((a v b') ^ (b ^ a')) = 0
2418, 232or 72 . . . . . . . . . . . . 13 (((a v b') ^ b') v ((a v b') ^ (b ^ a'))) = (b' v 0)
25 or0 102 . . . . . . . . . . . . 13 (b' v 0) = b'
2624, 25ax-r2 36 . . . . . . . . . . . 12 (((a v b') ^ b') v ((a v b') ^ (b ^ a'))) = b'
2712, 26ax-r2 36 . . . . . . . . . . 11 ((a v b') ^ (b' v (b ^ a'))) = b'
2827lan 77 . . . . . . . . . 10 (((b v a') ^ (b v a)) ^ ((a v b') ^ (b' v (b ^ a')))) = (((b v a') ^ (b v a)) ^ b')
29 ancom 74 . . . . . . . . . . 11 (((b v a') ^ (b v a)) ^ b') = (b' ^ ((b v a') ^ (b v a)))
30 anass 76 . . . . . . . . . . . 12 ((b' ^ (b v a')) ^ (b v a)) = (b' ^ ((b v a') ^ (b v a)))
3130ax-r1 35 . . . . . . . . . . 11 (b' ^ ((b v a') ^ (b v a))) = ((b' ^ (b v a')) ^ (b v a))
3229, 31ax-r2 36 . . . . . . . . . 10 (((b v a') ^ (b v a)) ^ b') = ((b' ^ (b v a')) ^ (b v a))
3328, 32ax-r2 36 . . . . . . . . 9 (((b v a') ^ (b v a)) ^ ((a v b') ^ (b' v (b ^ a')))) = ((b' ^ (b v a')) ^ (b v a))
346, 33ax-r2 36 . . . . . . . 8 ((a v b') ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) = ((b' ^ (b v a')) ^ (b v a))
3534ran 78 . . . . . . 7 (((a v b') ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) ^ (a v b)) = (((b' ^ (b v a')) ^ (b v a)) ^ (a v b))
36 ax-a2 31 . . . . . . . . 9 (a v b) = (b v a)
3736lan 77 . . . . . . . 8 (((b' ^ (b v a')) ^ (b v a)) ^ (a v b)) = (((b' ^ (b v a')) ^ (b v a)) ^ (b v a))
38 anass 76 . . . . . . . . 9 (((b' ^ (b v a')) ^ (b v a)) ^ (b v a)) = ((b' ^ (b v a')) ^ ((b v a) ^ (b v a)))
39 anidm 111 . . . . . . . . . . 11 ((b v a) ^ (b v a)) = (b v a)
4039lan 77 . . . . . . . . . 10 ((b' ^ (b v a')) ^ ((b v a) ^ (b v a))) = ((b' ^ (b v a')) ^ (b v a))
41 an32 83 . . . . . . . . . 10 ((b' ^ (b v a')) ^ (b v a)) = ((b' ^ (b v a)) ^ (b v a'))
4240, 41ax-r2 36 . . . . . . . . 9 ((b' ^ (b v a')) ^ ((b v a) ^ (b v a))) = ((b' ^ (b v a)) ^ (b v a'))
4338, 42ax-r2 36 . . . . . . . 8 (((b' ^ (b v a')) ^ (b v a)) ^ (b v a)) = ((b' ^ (b v a)) ^ (b v a'))
4437, 43ax-r2 36 . . . . . . 7 (((b' ^ (b v a')) ^ (b v a)) ^ (a v b)) = ((b' ^ (b v a)) ^ (b v a'))
4535, 44ax-r2 36 . . . . . 6 (((a v b') ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) ^ (a v b)) = ((b' ^ (b v a)) ^ (b v a'))
465, 45ax-r2 36 . . . . 5 (((a v b') ^ (a v b)) ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) = ((b' ^ (b v a)) ^ (b v a'))
4746ran 78 . . . 4 ((((a v b') ^ (a v b)) ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) ^ (a' v (a ^ b'))) = (((b' ^ (b v a)) ^ (b v a')) ^ (a' v (a ^ b')))
48 anass 76 . . . . 5 (((b' ^ (b v a)) ^ (b v a')) ^ (a' v (a ^ b'))) = ((b' ^ (b v a)) ^ ((b v a') ^ (a' v (a ^ b'))))
49 ax-a2 31 . . . . . . . . 9 (b v a') = (a' v b)
5049ran 78 . . . . . . . 8 ((b v a') ^ (a' v (a ^ b'))) = ((a' v b) ^ (a' v (a ^ b')))
51 ancom 74 . . . . . . . . 9 ((a' v b) ^ (a' v (a ^ b'))) = ((a' v (a ^ b')) ^ (a' v b))
52 comor1 461 . . . . . . . . . . 11 (a' v b) C a'
5352comcom7 460 . . . . . . . . . . . 12 (a' v b) C a
54 comor2 462 . . . . . . . . . . . . 13 (a' v b) C b
5554comcom2 183 . . . . . . . . . . . 12 (a' v b) C b'
5653, 55com2an 484 . . . . . . . . . . 11 (a' v b) C (a ^ b')
5752, 56fh1r 473 . . . . . . . . . 10 ((a' v (a ^ b')) ^ (a' v b)) = ((a' ^ (a' v b)) v ((a ^ b') ^ (a' v b)))
58 anabs 121 . . . . . . . . . . . 12 (a' ^ (a' v b)) = a'
59 ancom 74 . . . . . . . . . . . . 13 ((a ^ b') ^ (a' v b)) = ((a' v b) ^ (a ^ b'))
60 anor1 88 . . . . . . . . . . . . . . 15 (a ^ b') = (a' v b)'
6160lan 77 . . . . . . . . . . . . . 14 ((a' v b) ^ (a ^ b')) = ((a' v b) ^ (a' v b)')
62 dff 101 . . . . . . . . . . . . . . 15 0 = ((a' v b) ^ (a' v b)')
6362ax-r1 35 . . . . . . . . . . . . . 14 ((a' v b) ^ (a' v b)') = 0
6461, 63ax-r2 36 . . . . . . . . . . . . 13 ((a' v b) ^ (a ^ b')) = 0
6559, 64ax-r2 36 . . . . . . . . . . . 12 ((a ^ b') ^ (a' v b)) = 0
6658, 652or 72 . . . . . . . . . . 11 ((a' ^ (a' v b)) v ((a ^ b') ^ (a' v b))) = (a' v 0)
67 or0 102 . . . . . . . . . . 11 (a' v 0) = a'
6866, 67ax-r2 36 . . . . . . . . . 10 ((a' ^ (a' v b)) v ((a ^ b') ^ (a' v b))) = a'
6957, 68ax-r2 36 . . . . . . . . 9 ((a' v (a ^ b')) ^ (a' v b)) = a'
7051, 69ax-r2 36 . . . . . . . 8 ((a' v b) ^ (a' v (a ^ b'))) = a'
7150, 70ax-r2 36 . . . . . . 7 ((b v a') ^ (a' v (a ^ b'))) = a'
7271lan 77 . . . . . 6 ((b' ^ (b v a)) ^ ((b v a') ^ (a' v (a ^ b')))) = ((b' ^ (b v a)) ^ a')
73 an32 83 . . . . . . 7 ((b' ^ (b v a)) ^ a') = ((b' ^ a') ^ (b v a))
74 oran 87 . . . . . . . . 9 (b v a) = (b' ^ a')'
7574lan 77 . . . . . . . 8 ((b' ^ a') ^ (b v a)) = ((b' ^ a') ^ (b' ^ a')')
76 dff 101 . . . . . . . . 9 0 = ((b' ^ a') ^ (b' ^ a')')
7776ax-r1 35 . . . . . . . 8 ((b' ^ a') ^ (b' ^ a')') = 0
7875, 77ax-r2 36 . . . . . . 7 ((b' ^ a') ^ (b v a)) = 0
7973, 78ax-r2 36 . . . . . 6 ((b' ^ (b v a)) ^ a') = 0
8072, 79ax-r2 36 . . . . 5 ((b' ^ (b v a)) ^ ((b v a') ^ (a' v (a ^ b')))) = 0
8148, 80ax-r2 36 . . . 4 (((b' ^ (b v a)) ^ (b v a')) ^ (a' v (a ^ b'))) = 0
8247, 81ax-r2 36 . . 3 ((((a v b') ^ (a v b)) ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) ^ (a' v (a ^ b'))) = 0
834, 82ax-r2 36 . 2 ((((a v b') ^ (a v b)) ^ (a' v (a ^ b'))) ^ (((b v a') ^ (b v a)) ^ (b' v (b ^ a')))) = 0
843, 83ax-r2 36 1 ((a ->3 b)' ^ (b ->3 a)') = 0
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   v wo 6   ^ wa 7  0wf 9   ->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-i3 46  df-le1 130  df-le2 131  df-c1 132  df-c2 133
This theorem is referenced by:  ud3lem1  570
  Copyright terms: Public domain W3C validator