Theorem u3lemax4 778

Description: Possible axiom for Kalmbach implication system.

Assertion

Ref	Expression
u3lemax4	((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))))) = 1

Proof of Theorem u3lemax4

Step	Hyp	Ref	Expression
1		lem4 493	. 2 ((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))))) = ((a ->3 b)_|_ v ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))))
2		lem4 493	. . . . 5 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))) = ((b ->3 a)_|_ v ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))
3		lem4 493	. . . . . . 7 (c ->3 (c ->3 a)) = (c_|_ v a)
4		lem4 493	. . . . . . 7 (c ->3 (c ->3 b)) = (c_|_ v b)
5	3, 4	2i3 246	. . . . . 6 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))) = ((c_|_ v a) ->3 (c_|_ v b))
6	5	lor 66	. . . . 5 ((b ->3 a)_|_ v ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b)))) = ((b ->3 a)_|_ v ((c_|_ v a) ->3 (c_|_ v b)))
7	2, 6	ax-r2 35	. . . 4 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))) = ((b ->3 a)_|_ v ((c_|_ v a) ->3 (c_|_ v b)))
8	7	lor 66	. . 3 ((a ->3 b)_|_ v ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b)))))) = ((a ->3 b)_|_ v ((b ->3 a)_|_ v ((c_|_ v a) ->3 (c_|_ v b))))
9		oran3 85	. . . . . 6 ((a ->3 b)_|_ v (b ->3 a)_|_) = ((a ->3 b) ^ (b ->3 a))_|_
10		u3lembi 705	. . . . . . 7 ((a ->3 b) ^ (b ->3 a)) = (a == b)
11	10	ax-r4 36	. . . . . 6 ((a ->3 b) ^ (b ->3 a))_|_ = (a == b)_|_
12	9, 11	ax-r2 35	. . . . 5 ((a ->3 b)_|_ v (b ->3 a)_|_) = (a == b)_|_
13	12	ax-r5 37	. . . 4 (((a ->3 b)_|_ v (b ->3 a)_|_) v ((c_|_ v a) ->3 (c_|_ v b))) = ((a == b)_|_ v ((c_|_ v a) ->3 (c_|_ v b)))
14		ax-a3 31	. . . 4 (((a ->3 b)_|_ v (b ->3 a)_|_) v ((c_|_ v a) ->3 (c_|_ v b))) = ((a ->3 b)_|_ v ((b ->3 a)_|_ v ((c_|_ v a) ->3 (c_|_ v b))))
15		le1 138	. . . . 5 ((a == b)_|_ v ((c_|_ v a) ->3 (c_|_ v b))) =< 1
16		ska4 415	. . . . . . . 8 ((a_|_ == b_|_)_|_ v ((a_|_ ^ c) == (b_|_ ^ c))) = 1
17	16	ax-r1 34	. . . . . . 7 1 = ((a_|_ == b_|_)_|_ v ((a_|_ ^ c) == (b_|_ ^ c)))
18		conb 114	. . . . . . . . . 10 (a == b) = (a_|_ == b_|_)
19	18	ax-r4 36	. . . . . . . . 9 (a == b)_|_ = (a_|_ == b_|_)_|_
20		conb 114	. . . . . . . . . 10 ((c_|_ v a) == (c_|_ v b)) = ((c_|_ v a)_|_ == (c_|_ v b)_|_)
21		ancom 68	. . . . . . . . . . . . 13 (a_|_ ^ c) = (c ^ a_|_)
22		anor1 80	. . . . . . . . . . . . 13 (c ^ a_|_) = (c_|_ v a)_|_
23	21, 22	ax-r2 35	. . . . . . . . . . . 12 (a_|_ ^ c) = (c_|_ v a)_|_
24		ancom 68	. . . . . . . . . . . . 13 (b_|_ ^ c) = (c ^ b_|_)
25		anor1 80	. . . . . . . . . . . . 13 (c ^ b_|_) = (c_|_ v b)_|_
26	24, 25	ax-r2 35	. . . . . . . . . . . 12 (b_|_ ^ c) = (c_|_ v b)_|_
27	23, 26	2bi 91	. . . . . . . . . . 11 ((a_|_ ^ c) == (b_|_ ^ c)) = ((c_|_ v a)_|_ == (c_|_ v b)_|_)
28	27	ax-r1 34	. . . . . . . . . 10 ((c_|_ v a)_|_ == (c_|_ v b)_|_) = ((a_|_ ^ c) == (b_|_ ^ c))
29	20, 28	ax-r2 35	. . . . . . . . 9 ((c_|_ v a) == (c_|_ v b)) = ((a_|_ ^ c) == (b_|_ ^ c))
30	19, 29	2or 67	. . . . . . . 8 ((a == b)_|_ v ((c_|_ v a) == (c_|_ v b))) = ((a_|_ == b_|_)_|_ v ((a_|_ ^ c) == (b_|_ ^ c)))
31	30	ax-r1 34	. . . . . . 7 ((a_|_ == b_|_)_|_ v ((a_|_ ^ c) == (b_|_ ^ c))) = ((a == b)_|_ v ((c_|_ v a) == (c_|_ v b)))
32	17, 31	ax-r2 35	. . . . . 6 1 = ((a == b)_|_ v ((c_|_ v a) == (c_|_ v b)))
33		u3lembi 705	. . . . . . . . 9 (((c_|_ v a) ->3 (c_|_ v b)) ^ ((c_|_ v b) ->3 (c_|_ v a))) = ((c_|_ v a) == (c_|_ v b))
34	33	ax-r1 34	. . . . . . . 8 ((c_|_ v a) == (c_|_ v b)) = (((c_|_ v a) ->3 (c_|_ v b)) ^ ((c_|_ v b) ->3 (c_|_ v a)))
35		lea 152	. . . . . . . 8 (((c_|_ v a) ->3 (c_|_ v b)) ^ ((c_|_ v b) ->3 (c_|_ v a))) =< ((c_|_ v a) ->3 (c_|_ v b))
36	34, 35	bltr 130	. . . . . . 7 ((c_|_ v a) == (c_|_ v b)) =< ((c_|_ v a) ->3 (c_|_ v b))
37	36	lelor 158	. . . . . 6 ((a == b)_|_ v ((c_|_ v a) == (c_|_ v b))) =< ((a == b)_|_ v ((c_|_ v a) ->3 (c_|_ v b)))
38	32, 37	bltr 130	. . . . 5 1 =< ((a == b)_|_ v ((c_|_ v a) ->3 (c_|_ v b)))
39	15, 38	lebi 137	. . . 4 ((a == b)_|_ v ((c_|_ v a) ->3 (c_|_ v b))) = 1
40	13, 14, 39	3tr2 61	. . 3 ((a ->3 b)_|_ v ((b ->3 a)_|_ v ((c_|_ v a) ->3 (c_|_ v b)))) = 1
41	8, 40	ax-r2 35	. 2 ((a ->3 b)_|_ v ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b)))))) = 1
42	1, 41	ax-r2 35	1 ((a ->3 b) ->3 ((a ->3 b) ->3 ((b ->3 a) ->3 ((b ->3 a) ->3 ((c ->3 (c ->3 a)) ->3 (c ->3 (c ->3 b))))))) = 1

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

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  ax-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-i3 45  df-le 121  df-le1 122  df-le2 123  df-c1 124  df-c2 125  df-cmtr 126

metamath.org