Theorem ka4lemo 220

Description: Lemma for KA4 soundness (OR version) - uses OL only.

Assertion

Ref	Expression
ka4lemo	((a v b) v ((a v c) == (b v c))) = 1

Proof of Theorem ka4lemo

Step	Hyp	Ref	Expression
1		le1 138	. 2 ((a v b) v ((a v c) == (b v c))) =< 1
2		df-t 40	. . 3 1 = (((a v b) v c) v ((a v b) v c)_|_)
3		leo 150	. . . . . . 7 c =< (c v (a ^ b))
4		ax-a2 30	. . . . . . 7 (c v (a ^ b)) = ((a ^ b) v c)
5	3, 4	lbtr 131	. . . . . 6 c =< ((a ^ b) v c)
6	5	lelor 158	. . . . 5 ((a v b) v c) =< ((a v b) v ((a ^ b) v c))
7	6	leror 144	. . . 4 (((a v b) v c) v ((a v b) v c)_|_) =< (((a v b) v ((a ^ b) v c)) v ((a v b) v c)_|_)
8		ax-a3 31	. . . . 5 (((a v b) v ((a ^ b) v c)) v ((a v b) v c)_|_) = ((a v b) v (((a ^ b) v c) v ((a v b) v c)_|_))
9		ledio 168	. . . . . . . . 9 (c v (a ^ b)) =< ((c v a) ^ (c v b))
10		ax-a2 30	. . . . . . . . 9 ((a ^ b) v c) = (c v (a ^ b))
11		ax-a2 30	. . . . . . . . . 10 (a v c) = (c v a)
12		ax-a2 30	. . . . . . . . . 10 (b v c) = (c v b)
13	11, 12	2an 72	. . . . . . . . 9 ((a v c) ^ (b v c)) = ((c v a) ^ (c v b))
14	9, 10, 13	le3tr1 132	. . . . . . . 8 ((a ^ b) v c) =< ((a v c) ^ (b v c))
15	14	leror 144	. . . . . . 7 (((a ^ b) v c) v ((a v b) v c)_|_) =< (((a v c) ^ (b v c)) v ((a v b) v c)_|_)
16		dfb 86	. . . . . . . . 9 ((a v c) == (b v c)) = (((a v c) ^ (b v c)) v ((a v c)_|_ ^ (b v c)_|_))
17		oran 79	. . . . . . . . . . . . 13 (a v c) = (a_|_ ^ c_|_)_|_
18	17	con2 64	. . . . . . . . . . . 12 (a v c)_|_ = (a_|_ ^ c_|_)
19		oran 79	. . . . . . . . . . . . 13 (b v c) = (b_|_ ^ c_|_)_|_
20	19	con2 64	. . . . . . . . . . . 12 (b v c)_|_ = (b_|_ ^ c_|_)
21	18, 20	2an 72	. . . . . . . . . . 11 ((a v c)_|_ ^ (b v c)_|_) = ((a_|_ ^ c_|_) ^ (b_|_ ^ c_|_))
22		anor1 80	. . . . . . . . . . . 12 ((a_|_ ^ b_|_) ^ c_|_) = ((a_|_ ^ b_|_)_|_ v c)_|_
23		anandir 107	. . . . . . . . . . . . 13 ((a_|_ ^ b_|_) ^ c_|_) = ((a_|_ ^ c_|_) ^ (b_|_ ^ c_|_))
24	23	ax-r1 34	. . . . . . . . . . . 12 ((a_|_ ^ c_|_) ^ (b_|_ ^ c_|_)) = ((a_|_ ^ b_|_) ^ c_|_)
25		oran 79	. . . . . . . . . . . . . 14 (a v b) = (a_|_ ^ b_|_)_|_
26	25	ax-r5 37	. . . . . . . . . . . . 13 ((a v b) v c) = ((a_|_ ^ b_|_)_|_ v c)
27	26	ax-r4 36	. . . . . . . . . . . 12 ((a v b) v c)_|_ = ((a_|_ ^ b_|_)_|_ v c)_|_
28	22, 24, 27	3tr1 60	. . . . . . . . . . 11 ((a_|_ ^ c_|_) ^ (b_|_ ^ c_|_)) = ((a v b) v c)_|_
29	21, 28	ax-r2 35	. . . . . . . . . 10 ((a v c)_|_ ^ (b v c)_|_) = ((a v b) v c)_|_
30	29	lor 66	. . . . . . . . 9 (((a v c) ^ (b v c)) v ((a v c)_|_ ^ (b v c)_|_)) = (((a v c) ^ (b v c)) v ((a v b) v c)_|_)
31	16, 30	ax-r2 35	. . . . . . . 8 ((a v c) == (b v c)) = (((a v c) ^ (b v c)) v ((a v b) v c)_|_)
32	31	ax-r1 34	. . . . . . 7 (((a v c) ^ (b v c)) v ((a v b) v c)_|_) = ((a v c) == (b v c))
33	15, 32	lbtr 131	. . . . . 6 (((a ^ b) v c) v ((a v b) v c)_|_) =< ((a v c) == (b v c))
34	33	lelor 158	. . . . 5 ((a v b) v (((a ^ b) v c) v ((a v b) v c)_|_)) =< ((a v b) v ((a v c) == (b v c)))
35	8, 34	bltr 130	. . . 4 (((a v b) v ((a ^ b) v c)) v ((a v b) v c)_|_) =< ((a v b) v ((a v c) == (b v c)))
36	7, 35	letr 129	. . 3 (((a v b) v c) v ((a v b) v c)_|_) =< ((a v b) v ((a v c) == (b v c)))
37	2, 36	bltr 130	. 2 1 =< ((a v b) v ((a v c) == (b v c)))
38	1, 37	lebi 137	1 ((a v b) v ((a v c) == (b v c))) = 1

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v wo 6   ^ wa 7  1wt 9

This theorem is referenced by:  ka4lem 221  wr5 413  ka4ot 417

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

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

metamath.org