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

Step	Hyp	Ref	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)'))
3	2	ax-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)'
7	6	lan 77	. . . . . . 7 (a' ^ (b' ^ c')) = (a' ^ (b v c)')
8	5, 7	ax-r2 36	. . . . . 6 ((a' ^ b') ^ c') = (a' ^ (b v c)')
9		anor3 90	. . . . . . 7 (a' ^ c') = (a v c)'
10	9, 6	2an 79	. . . . . 6 ((a' ^ c') ^ (b' ^ c')) = ((a v c)' ^ (b v c)')
11	4, 8, 10	3tr2 64	. . . . 5 (a' ^ (b v c)') = ((a v c)' ^ (b v c)')
12	11	lor 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
16	14, 15	skr0 242	. . . . . . . . . . . . 13 ((a ->1 b) ^ (b ->1 a)) = 1
17	16	ax-r1 35	. . . . . . . . . . . 12 1 = ((a ->1 b) ^ (b ->1 a))
18		lea 160	. . . . . . . . . . . 12 ((a ->1 b) ^ (b ->1 a)) =< (a ->1 b)
19	17, 18	bltr 138	. . . . . . . . . . 11 1 =< (a ->1 b)
20		le1 146	. . . . . . . . . . 11 (a ->1 b) =< 1
21	19, 20	lebi 145	. . . . . . . . . 10 1 = (a ->1 b)
22		df-i1 44	. . . . . . . . . 10 (a ->1 b) = (a' v (a ^ b))
23	21, 22	ax-r2 36	. . . . . . . . 9 1 = (a' v (a ^ b))
24		leo 158	. . . . . . . . . . 11 b =< (b v c)
25	24	lelan 167	. . . . . . . . . 10 (a ^ b) =< (a ^ (b v c))
26	25	lelor 166	. . . . . . . . 9 (a' v (a ^ b)) =< (a' v (a ^ (b v c)))
27	23, 26	bltr 138	. . . . . . . 8 1 =< (a' v (a ^ (b v c)))
28		le1 146	. . . . . . . 8 (a' v (a ^ (b v c))) =< 1
29	27, 28	lebi 145	. . . . . . 7 1 = (a' v (a ^ (b v c)))
30	29	ax-r1 35	. . . . . 6 (a' v (a ^ (b v c))) = 1
31	13, 30	ax-r2 36	. . . . 5 (a ->1 (b v c)) = 1
32	31	2vwomr1a 363	. . . 4 (a ->2 (b v c)) = 1
33	3, 12, 32	3tr2 64	. . 3 ((b v c) v ((a v c)' ^ (b v c)')) = 1
34	1, 33	ax-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)'))
37	36	ax-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'))
40	9	lan 77	. . . . . . 7 (b' ^ (a' ^ c')) = (b' ^ (a v c)')
41	39, 40	ax-r2 36	. . . . . 6 ((b' ^ a') ^ c') = (b' ^ (a v c)')
42	6, 9	2an 79	. . . . . 6 ((b' ^ c') ^ (a' ^ c')) = ((b v c)' ^ (a v c)')
43	38, 41, 42	3tr2 64	. . . . 5 (b' ^ (a v c)') = ((b v c)' ^ (a v c)')
44	43	lor 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)
47	17, 46	bltr 138	. . . . . . . . . . 11 1 =< (b ->1 a)
48		le1 146	. . . . . . . . . . 11 (b ->1 a) =< 1
49	47, 48	lebi 145	. . . . . . . . . 10 1 = (b ->1 a)
50		df-i1 44	. . . . . . . . . 10 (b ->1 a) = (b' v (b ^ a))
51	49, 50	ax-r2 36	. . . . . . . . 9 1 = (b' v (b ^ a))
52		leo 158	. . . . . . . . . . 11 a =< (a v c)
53	52	lelan 167	. . . . . . . . . 10 (b ^ a) =< (b ^ (a v c))
54	53	lelor 166	. . . . . . . . 9 (b' v (b ^ a)) =< (b' v (b ^ (a v c)))
55	51, 54	bltr 138	. . . . . . . 8 1 =< (b' v (b ^ (a v c)))
56		le1 146	. . . . . . . 8 (b' v (b ^ (a v c))) =< 1
57	55, 56	lebi 145	. . . . . . 7 1 = (b' v (b ^ (a v c)))
58	57	ax-r1 35	. . . . . 6 (b' v (b ^ (a v c))) = 1
59	45, 58	ax-r2 36	. . . . 5 (b ->1 (a v c)) = 1
60	59	2vwomr1a 363	. . . 4 (b ->2 (a v c)) = 1
61	37, 44, 60	3tr2 64	. . 3 ((a v c) v ((b v c)' ^ (a v c)')) = 1
62	35, 61	ax-r2 36	. 2 ((b v c) ->2 (a v c)) = 1
63	34, 62	2vwomlem 365	1 ((a v c) == (b v c)) = 1

Syntax hints:   = wb 1  'wn 4   == tb 5   v wo 6   ^ wa 7  1wt 8   ->1 wi1 12   ->2 wi2 13

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

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

Copyright terms: Public domain