QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  2vwomlem Unicode version
Theorem 2vwomlem 365
Description: Lemma from 2-variable WOML rule.
Hypotheses
Ref Expression
2vwomlem.1 (a ->2 b) = 1
2vwomlem.2 (b ->2 a) = 1
Assertion
Ref Expression
2vwomlem (a == b) = 1
Proof of Theorem 2vwomlem
StepHypRef Expression
1 dfb 94 . 2 (a == b) = ((a ^ b) v (a' ^ b'))
2 df-f 42 . . . . 5 0 = 1'
3 anor2 89 . . . . . . 7 (a' ^ (a v b)) = (a v (a v b)')'
43ax-r1 35 . . . . . 6 (a v (a v b)')' = (a' ^ (a v b))
5 anor3 90 . . . . . . . . . . 11 (a' ^ b') = (a v b)'
65ax-r1 35 . . . . . . . . . 10 (a v b)' = (a' ^ b')
7 ancom 74 . . . . . . . . . 10 (a' ^ b') = (b' ^ a')
86, 7ax-r2 36 . . . . . . . . 9 (a v b)' = (b' ^ a')
98lor 70 . . . . . . . 8 (a v (a v b)') = (a v (b' ^ a'))
10 df-i2 45 . . . . . . . . 9 (b ->2 a) = (a v (b' ^ a'))
1110ax-r1 35 . . . . . . . 8 (a v (b' ^ a')) = (b ->2 a)
12 2vwomlem.2 . . . . . . . 8 (b ->2 a) = 1
139, 11, 123tr 65 . . . . . . 7 (a v (a v b)') = 1
1413ax-r4 37 . . . . . 6 (a v (a v b)')' = 1'
15 anabs 121 . . . . . . . . 9 (a' ^ (a' v b')) = a'
1615ax-r1 35 . . . . . . . 8 a' = (a' ^ (a' v b'))
1716ran 78 . . . . . . 7 (a' ^ (a v b)) = ((a' ^ (a' v b')) ^ (a v b))
18 anass 76 . . . . . . 7 ((a' ^ (a' v b')) ^ (a v b)) = (a' ^ ((a' v b') ^ (a v b)))
19 oran3 93 . . . . . . . . . 10 (a' v b') = (a ^ b)'
20 oran 87 . . . . . . . . . 10 (a v b) = (a' ^ b')'
2119, 202an 79 . . . . . . . . 9 ((a' v b') ^ (a v b)) = ((a ^ b)' ^ (a' ^ b')')
22 anor3 90 . . . . . . . . 9 ((a ^ b)' ^ (a' ^ b')') = ((a ^ b) v (a' ^ b'))'
2321, 22ax-r2 36 . . . . . . . 8 ((a' v b') ^ (a v b)) = ((a ^ b) v (a' ^ b'))'
2423lan 77 . . . . . . 7 (a' ^ ((a' v b') ^ (a v b))) = (a' ^ ((a ^ b) v (a' ^ b'))')
2517, 18, 243tr 65 . . . . . 6 (a' ^ (a v b)) = (a' ^ ((a ^ b) v (a' ^ b'))')
264, 14, 253tr2 64 . . . . 5 1' = (a' ^ ((a ^ b) v (a' ^ b'))')
272, 26ax-r2 36 . . . 4 0 = (a' ^ ((a ^ b) v (a' ^ b'))')
2827lor 70 . . 3 (((a ^ b) v (a' ^ b')) v 0) = (((a ^ b) v (a' ^ b')) v (a' ^ ((a ^ b) v (a' ^ b'))'))
29 or0 102 . . 3 (((a ^ b) v (a' ^ b')) v 0) = ((a ^ b) v (a' ^ b'))
30 le1 146 . . . . 5 (a' v (a ^ ((a ^ b) v (a' ^ b')))) =< 1
31 df-i2 45 . . . . . . . . . 10 (a ->2 b) = (b v (a' ^ b'))
3231ax-r1 35 . . . . . . . . 9 (b v (a' ^ b')) = (a ->2 b)
33 2vwomlem.1 . . . . . . . . 9 (a ->2 b) = 1
3432, 33ax-r2 36 . . . . . . . 8 (b v (a' ^ b')) = 1
35342vwomr2 362 . . . . . . 7 (a' v (a ^ b)) = 1
3635ax-r1 35 . . . . . 6 1 = (a' v (a ^ b))
37 lea 160 . . . . . . . 8 (a ^ b) =< a
38 leo 158 . . . . . . . 8 (a ^ b) =< ((a ^ b) v (a' ^ b'))
3937, 38ler2an 173 . . . . . . 7 (a ^ b) =< (a ^ ((a ^ b) v (a' ^ b')))
4039lelor 166 . . . . . 6 (a' v (a ^ b)) =< (a' v (a ^ ((a ^ b) v (a' ^ b'))))
4136, 40bltr 138 . . . . 5 1 =< (a' v (a ^ ((a ^ b) v (a' ^ b'))))
4230, 41lebi 145 . . . 4 (a' v (a ^ ((a ^ b) v (a' ^ b')))) = 1
4342ax-wom 361 . . 3 (((a ^ b) v (a' ^ b')) v (a' ^ ((a ^ b) v (a' ^ b'))')) = 1
4428, 29, 433tr2 64 . 2 ((a ^ b) v (a' ^ b')) = 1
451, 44ax-r2 36 1 (a == b) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8  0wf 9   ->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-wom 361
This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i2 45  df-le1 130  df-le2 131
This theorem is referenced by:  wr5-2v  366
  Copyright terms: Public domain W3C validator