Theorem wr5-2v 348

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 44	. . 3 ((a v c) ->2 (b v c)) = ((b v c) v ((a v c)_|_ ^ (b v c)_|_))
2		df-i2 44	. . . . 5 (a ->2 (b v c)) = ((b v c) v (a_|_ ^ (b v c)_|_))
3	2	ax-r1 34	. . . 4 ((b v c) v (a_|_ ^ (b v c)_|_)) = (a ->2 (b v c))
4		anandir 107	. . . . . 6 ((a_|_ ^ b_|_) ^ c_|_) = ((a_|_ ^ c_|_) ^ (b_|_ ^ c_|_))
5		anass 69	. . . . . . 7 ((a_|_ ^ b_|_) ^ c_|_) = (a_|_ ^ (b_|_ ^ c_|_))
6		anor3 82	. . . . . . . 8 (b_|_ ^ c_|_) = (b v c)_|_
7	6	lan 70	. . . . . . 7 (a_|_ ^ (b_|_ ^ c_|_)) = (a_|_ ^ (b v c)_|_)
8	5, 7	ax-r2 35	. . . . . 6 ((a_|_ ^ b_|_) ^ c_|_) = (a_|_ ^ (b v c)_|_)
9		anor3 82	. . . . . . 7 (a_|_ ^ c_|_) = (a v c)_|_
10	9, 6	2an 72	. . . . . 6 ((a_|_ ^ c_|_) ^ (b_|_ ^ c_|_)) = ((a v c)_|_ ^ (b v c)_|_)
11	4, 8, 10	3tr2 61	. . . . 5 (a_|_ ^ (b v c)_|_) = ((a v c)_|_ ^ (b v c)_|_)
12	11	lor 66	. . . 4 ((b v c) v (a_|_ ^ (b v c)_|_)) = ((b v c) v ((a v c)_|_ ^ (b v c)_|_))
13		df-i1 43	. . . . . 6 (a ->1 (b v c)) = (a_|_ v (a ^ (b v c)))
14		wr5-2v.1	. . . . . . . . . . . . . 14 (a == b) = 1
15		wlem1 235	. . . . . . . . . . . . . 14 ((a == b)_|_ v ((a ->1 b) ^ (b ->1 a))) = 1
16	14, 15	skr0 234	. . . . . . . . . . . . 13 ((a ->1 b) ^ (b ->1 a)) = 1
17	16	ax-r1 34	. . . . . . . . . . . 12 1 = ((a ->1 b) ^ (b ->1 a))
18		lea 152	. . . . . . . . . . . 12 ((a ->1 b) ^ (b ->1 a)) =< (a ->1 b)
19	17, 18	bltr 130	. . . . . . . . . . 11 1 =< (a ->1 b)
20		le1 138	. . . . . . . . . . 11 (a ->1 b) =< 1
21	19, 20	lebi 137	. . . . . . . . . 10 1 = (a ->1 b)
22		df-i1 43	. . . . . . . . . 10 (a ->1 b) = (a_|_ v (a ^ b))
23	21, 22	ax-r2 35	. . . . . . . . 9 1 = (a_|_ v (a ^ b))
24		leo 150	. . . . . . . . . . 11 b =< (b v c)
25	24	lelan 159	. . . . . . . . . 10 (a ^ b) =< (a ^ (b v c))
26	25	lelor 158	. . . . . . . . 9 (a_|_ v (a ^ b)) =< (a_|_ v (a ^ (b v c)))
27	23, 26	bltr 130	. . . . . . . 8 1 =< (a_|_ v (a ^ (b v c)))
28		le1 138	. . . . . . . 8 (a_|_ v (a ^ (b v c))) =< 1
29	27, 28	lebi 137	. . . . . . 7 1 = (a_|_ v (a ^ (b v c)))
30	29	ax-r1 34	. . . . . 6 (a_|_ v (a ^ (b v c))) = 1
31	13, 30	ax-r2 35	. . . . 5 (a ->1 (b v c)) = 1
32	31	2vwomr1a 345	. . . 4 (a ->2 (b v c)) = 1
33	3, 12, 32	3tr2 61	. . 3 ((b v c) v ((a v c)_|_ ^ (b v c)_|_)) = 1
34	1, 33	ax-r2 35	. 2 ((a v c) ->2 (b v c)) = 1
35		df-i2 44	. . 3 ((b v c) ->2 (a v c)) = ((a v c) v ((b v c)_|_ ^ (a v c)_|_))
36		df-i2 44	. . . . 5 (b ->2 (a v c)) = ((a v c) v (b_|_ ^ (a v c)_|_))
37	36	ax-r1 34	. . . 4 ((a v c) v (b_|_ ^ (a v c)_|_)) = (b ->2 (a v c))
38		anandir 107	. . . . . 6 ((b_|_ ^ a_|_) ^ c_|_) = ((b_|_ ^ c_|_) ^ (a_|_ ^ c_|_))
39		anass 69	. . . . . . 7 ((b_|_ ^ a_|_) ^ c_|_) = (b_|_ ^ (a_|_ ^ c_|_))
40	9	lan 70	. . . . . . 7 (b_|_ ^ (a_|_ ^ c_|_)) = (b_|_ ^ (a v c)_|_)
41	39, 40	ax-r2 35	. . . . . 6 ((b_|_ ^ a_|_) ^ c_|_) = (b_|_ ^ (a v c)_|_)
42	6, 9	2an 72	. . . . . 6 ((b_|_ ^ c_|_) ^ (a_|_ ^ c_|_)) = ((b v c)_|_ ^ (a v c)_|_)
43	38, 41, 42	3tr2 61	. . . . 5 (b_|_ ^ (a v c)_|_) = ((b v c)_|_ ^ (a v c)_|_)
44	43	lor 66	. . . 4 ((a v c) v (b_|_ ^ (a v c)_|_)) = ((a v c) v ((b v c)_|_ ^ (a v c)_|_))
45		df-i1 43	. . . . . 6 (b ->1 (a v c)) = (b_|_ v (b ^ (a v c)))
46		lear 153	. . . . . . . . . . . 12 ((a ->1 b) ^ (b ->1 a)) =< (b ->1 a)
47	17, 46	bltr 130	. . . . . . . . . . 11 1 =< (b ->1 a)
48		le1 138	. . . . . . . . . . 11 (b ->1 a) =< 1
49	47, 48	lebi 137	. . . . . . . . . 10 1 = (b ->1 a)
50		df-i1 43	. . . . . . . . . 10 (b ->1 a) = (b_|_ v (b ^ a))
51	49, 50	ax-r2 35	. . . . . . . . 9 1 = (b_|_ v (b ^ a))
52		leo 150	. . . . . . . . . . 11 a =< (a v c)
53	52	lelan 159	. . . . . . . . . 10 (b ^ a) =< (b ^ (a v c))
54	53	lelor 158	. . . . . . . . 9 (b_|_ v (b ^ a)) =< (b_|_ v (b ^ (a v c)))
55	51, 54	bltr 130	. . . . . . . 8 1 =< (b_|_ v (b ^ (a v c)))
56		le1 138	. . . . . . . 8 (b_|_ v (b ^ (a v c))) =< 1
57	55, 56	lebi 137	. . . . . . 7 1 = (b_|_ v (b ^ (a v c)))
58	57	ax-r1 34	. . . . . 6 (b_|_ v (b ^ (a v c))) = 1
59	45, 58	ax-r2 35	. . . . 5 (b ->1 (a v c)) = 1
60	59	2vwomr1a 345	. . . 4 (b ->2 (a v c)) = 1
61	37, 44, 60	3tr2 61	. . 3 ((a v c) v ((b v c)_|_ ^ (a v c)_|_)) = 1
62	35, 61	ax-r2 35	. 2 ((b v c) ->2 (a v c)) = 1
63	34, 62	2vwomlem 347	1 ((a v c) == (b v c)) = 1

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v wo 6   ^ wa 7  1wt 9   ->1 wi1 13   ->2 wi2 14

This theorem is referenced by:  wom3 349  wlor 350  wran 351  wr2 353  w2or 354  wler 373  wleror 375  wletr 378  wbltr 379  wbile 383  wlecom 391  wcomcom2 397  wfh2 406  ska2 414  woml6 418  woml7 419

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-wom 343

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le1 122  df-le2 123

metamath.org