QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  wr5-2v Unicode version
Theorem wr5-2v 366
Description: WOML derived from 2-variable axioms.
Hypothesis
Ref Expression
wr5-2v.1 (a == b) = 1
Assertion
Ref Expression
wr5-2v ((a v c) == (b v c)) = 1
Proof of Theorem wr5-2v
StepHypRef Expression
1 df-i2 45 . . 3 ((a v c) ->2 (b v c)) = ((b v c) v ((a v c)' ^ (b v c)'))
2 df-i2 45 . . . . 5 (a ->2 (b v c)) = ((b v c) v (a' ^ (b v c)'))
32ax-r1 35 . . . 4 ((b v c) v (a' ^ (b v c)')) = (a ->2 (b v c))
4 anandir 115 . . . . . 6 ((a' ^ b') ^ c') = ((a' ^ c') ^ (b' ^ c'))
5 anass 76 . . . . . . 7 ((a' ^ b') ^ c') = (a' ^ (b' ^ c'))
6 anor3 90 . . . . . . . 8 (b' ^ c') = (b v c)'
76lan 77 . . . . . . 7 (a' ^ (b' ^ c')) = (a' ^ (b v c)')
85, 7ax-r2 36 . . . . . 6 ((a' ^ b') ^ c') = (a' ^ (b v c)')
9 anor3 90 . . . . . . 7 (a' ^ c') = (a v c)'
109, 62an 79 . . . . . 6 ((a' ^ c') ^ (b' ^ c')) = ((a v c)' ^ (b v c)')
114, 8, 103tr2 64 . . . . 5 (a' ^ (b v c)') = ((a v c)' ^ (b v c)')
1211lor 70 . . . 4 ((b v c) v (a' ^ (b v c)')) = ((b v c) v ((a v c)' ^ (b v c)'))
13 df-i1 44 . . . . . 6 (a ->1 (b v c)) = (a' v (a ^ (b v c)))
14 wr5-2v.1 . . . . . . . . . . . . . 14 (a == b) = 1
15 wlem1 243 . . . . . . . . . . . . . 14 ((a == b)' v ((a ->1 b) ^ (b ->1 a))) = 1
1614, 15skr0 242 . . . . . . . . . . . . 13 ((a ->1 b) ^ (b ->1 a)) = 1
1716ax-r1 35 . . . . . . . . . . . 12 1 = ((a ->1 b) ^ (b ->1 a))
18 lea 160 . . . . . . . . . . . 12 ((a ->1 b) ^ (b ->1 a)) =< (a ->1 b)
1917, 18bltr 138 . . . . . . . . . . 11 1 =< (a ->1 b)
20 le1 146 . . . . . . . . . . 11 (a ->1 b) =< 1
2119, 20lebi 145 . . . . . . . . . 10 1 = (a ->1 b)
22 df-i1 44 . . . . . . . . . 10 (a ->1 b) = (a' v (a ^ b))
2321, 22ax-r2 36 . . . . . . . . 9 1 = (a' v (a ^ b))
24 leo 158 . . . . . . . . . . 11 b =< (b v c)
2524lelan 167 . . . . . . . . . 10 (a ^ b) =< (a ^ (b v c))
2625lelor 166 . . . . . . . . 9 (a' v (a ^ b)) =< (a' v (a ^ (b v c)))
2723, 26bltr 138 . . . . . . . 8 1 =< (a' v (a ^ (b v c)))
28 le1 146 . . . . . . . 8 (a' v (a ^ (b v c))) =< 1
2927, 28lebi 145 . . . . . . 7 1 = (a' v (a ^ (b v c)))
3029ax-r1 35 . . . . . 6 (a' v (a ^ (b v c))) = 1
3113, 30ax-r2 36 . . . . 5 (a ->1 (b v c)) = 1
32312vwomr1a 363 . . . 4 (a ->2 (b v c)) = 1
333, 12, 323tr2 64 . . 3 ((b v c) v ((a v c)' ^ (b v c)')) = 1
341, 33ax-r2 36 . 2 ((a v c) ->2 (b v c)) = 1
35 df-i2 45 . . 3 ((b v c) ->2 (a v c)) = ((a v c) v ((b v c)' ^ (a v c)'))
36 df-i2 45 . . . . 5 (b ->2 (a v c)) = ((a v c) v (b' ^ (a v c)'))
3736ax-r1 35 . . . 4 ((a v c) v (b' ^ (a v c)')) = (b ->2 (a v c))
38 anandir 115 . . . . . 6 ((b' ^ a') ^ c') = ((b' ^ c') ^ (a' ^ c'))
39 anass 76 . . . . . . 7 ((b' ^ a') ^ c') = (b' ^ (a' ^ c'))
409lan 77 . . . . . . 7 (b' ^ (a' ^ c')) = (b' ^ (a v c)')
4139, 40ax-r2 36 . . . . . 6 ((b' ^ a') ^ c') = (b' ^ (a v c)')
426, 92an 79 . . . . . 6 ((b' ^ c') ^ (a' ^ c')) = ((b v c)' ^ (a v c)')
4338, 41, 423tr2 64 . . . . 5 (b' ^ (a v c)') = ((b v c)' ^ (a v c)')
4443lor 70 . . . 4 ((a v c) v (b' ^ (a v c)')) = ((a v c) v ((b v c)' ^ (a v c)'))
45 df-i1 44 . . . . . 6 (b ->1 (a v c)) = (b' v (b ^ (a v c)))
46 lear 161 . . . . . . . . . . . 12 ((a ->1 b) ^ (b ->1 a)) =< (b ->1 a)
4717, 46bltr 138 . . . . . . . . . . 11 1 =< (b ->1 a)
48 le1 146 . . . . . . . . . . 11 (b ->1 a) =< 1
4947, 48lebi 145 . . . . . . . . . 10 1 = (b ->1 a)
50 df-i1 44 . . . . . . . . . 10 (b ->1 a) = (b' v (b ^ a))
5149, 50ax-r2 36 . . . . . . . . 9 1 = (b' v (b ^ a))
52 leo 158 . . . . . . . . . . 11 a =< (a v c)
5352lelan 167 . . . . . . . . . 10 (b ^ a) =< (b ^ (a v c))
5453lelor 166 . . . . . . . . 9 (b' v (b ^ a)) =< (b' v (b ^ (a v c)))
5551, 54bltr 138 . . . . . . . 8 1 =< (b' v (b ^ (a v c)))
56 le1 146 . . . . . . . 8 (b' v (b ^ (a v c))) =< 1
5755, 56lebi 145 . . . . . . 7 1 = (b' v (b ^ (a v c)))
5857ax-r1 35 . . . . . 6 (b' v (b ^ (a v c))) = 1
5945, 58ax-r2 36 . . . . 5 (b ->1 (a v c)) = 1
60592vwomr1a 363 . . . 4 (b ->2 (a v c)) = 1
6137, 44, 603tr2 64 . . 3 ((a v c) v ((b v c)' ^ (a v c)')) = 1
6235, 61ax-r2 36 . 2 ((b v c) ->2 (a v c)) = 1
6334, 622vwomlem 365 1 ((a v c) == (b v c)) = 1
Colors of variables: term
Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8   ->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-wom 361
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
This theorem is referenced by:  wom3  367  wlor  368  wran  369  wr2  371  w2or  372  wler  391  wleror  393  wletr  396  wbltr  397  wbile  401  wlecom  409  wcomcom2  415  wfh2  424  wr5  431  ska2  432  woml6  436  woml7  437
  Copyright terms: Public domain W3C validator