Theorem ka4lemo 228

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 146	. 2 ((a v b) v ((a v c) == (b v c))) =< 1
2		df-t 41	. . 3 1 = (((a v b) v c) v ((a v b) v c)')
3		leo 158	. . . . . . 7 c =< (c v (a ^ b))
4		ax-a2 31	. . . . . . 7 (c v (a ^ b)) = ((a ^ b) v c)
5	3, 4	lbtr 139	. . . . . 6 c =< ((a ^ b) v c)
6	5	lelor 166	. . . . 5 ((a v b) v c) =< ((a v b) v ((a ^ b) v c))
7	6	leror 152	. . . 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 32	. . . . 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 176	. . . . . . . . 9 (c v (a ^ b)) =< ((c v a) ^ (c v b))
10		ax-a2 31	. . . . . . . . 9 ((a ^ b) v c) = (c v (a ^ b))
11		ax-a2 31	. . . . . . . . . 10 (a v c) = (c v a)
12		ax-a2 31	. . . . . . . . . 10 (b v c) = (c v b)
13	11, 12	2an 79	. . . . . . . . 9 ((a v c) ^ (b v c)) = ((c v a) ^ (c v b))
14	9, 10, 13	le3tr1 140	. . . . . . . 8 ((a ^ b) v c) =< ((a v c) ^ (b v c))
15	14	leror 152	. . . . . . 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 94	. . . . . . . . 9 ((a v c) == (b v c)) = (((a v c) ^ (b v c)) v ((a v c)' ^ (b v c)'))
17		oran 87	. . . . . . . . . . . . 13 (a v c) = (a' ^ c')'
18	17	con2 67	. . . . . . . . . . . 12 (a v c)' = (a' ^ c')
19		oran 87	. . . . . . . . . . . . 13 (b v c) = (b' ^ c')'
20	19	con2 67	. . . . . . . . . . . 12 (b v c)' = (b' ^ c')
21	18, 20	2an 79	. . . . . . . . . . 11 ((a v c)' ^ (b v c)') = ((a' ^ c') ^ (b' ^ c'))
22		anor1 88	. . . . . . . . . . . 12 ((a' ^ b') ^ c') = ((a' ^ b')' v c)'
23		anandir 115	. . . . . . . . . . . . 13 ((a' ^ b') ^ c') = ((a' ^ c') ^ (b' ^ c'))
24	23	ax-r1 35	. . . . . . . . . . . 12 ((a' ^ c') ^ (b' ^ c')) = ((a' ^ b') ^ c')
25		oran 87	. . . . . . . . . . . . . 14 (a v b) = (a' ^ b')'
26	25	ax-r5 38	. . . . . . . . . . . . 13 ((a v b) v c) = ((a' ^ b')' v c)
27	26	ax-r4 37	. . . . . . . . . . . 12 ((a v b) v c)' = ((a' ^ b')' v c)'
28	22, 24, 27	3tr1 63	. . . . . . . . . . 11 ((a' ^ c') ^ (b' ^ c')) = ((a v b) v c)'
29	21, 28	ax-r2 36	. . . . . . . . . 10 ((a v c)' ^ (b v c)') = ((a v b) v c)'
30	29	lor 70	. . . . . . . . 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 36	. . . . . . . 8 ((a v c) == (b v c)) = (((a v c) ^ (b v c)) v ((a v b) v c)')
32	31	ax-r1 35	. . . . . . 7 (((a v c) ^ (b v c)) v ((a v b) v c)') = ((a v c) == (b v c))
33	15, 32	lbtr 139	. . . . . 6 (((a ^ b) v c) v ((a v b) v c)') =< ((a v c) == (b v c))
34	33	lelor 166	. . . . 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 138	. . . 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 137	. . 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 138	. 2 1 =< ((a v b) v ((a v c) == (b v c)))
38	1, 37	lebi 145	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 8

This theorem is referenced by:  ka4lem 229  ka4ot 435

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131

Copyright terms: Public domain