Theorem i3con 533

Description: Theorem for Kalmbach implication.

Assertion

Ref	Expression
i3con	((a ->3 b) ->3 ((a ->3 b) ->3 (b_|_ ->3 a_|_))) = 1

Proof of Theorem i3con

Step	Hyp	Ref	Expression
1		ni32 484	. . . . 5 (a ->3 b)_|_ = ((a v b) ^ ((a ^ b_|_) v (a_|_ ^ (a v b_|_))))
2		i3n1 241	. . . . 5 (b_|_ ->3 a_|_) = (((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_)))
3	1, 2	2or 67	. . . 4 ((a ->3 b)_|_ v (b_|_ ->3 a_|_)) = (((a v b) ^ ((a ^ b_|_) v (a_|_ ^ (a v b_|_)))) v (((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_))))
4		ax-a2 30	. . . . 5 (((a v b) ^ ((a ^ b_|_) v (a_|_ ^ (a v b_|_)))) v (((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_)))) = ((((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_))) v ((a v b) ^ ((a ^ b_|_) v (a_|_ ^ (a v b_|_)))))
5		comor2 444	. . . . . . . . . 10 (a v b) C b
6		comor1 443	. . . . . . . . . . 11 (a v b) C a
7	6	comcom2 175	. . . . . . . . . 10 (a v b) C a_|_
8	5, 7	com2an 466	. . . . . . . . 9 (a v b) C (b ^ a_|_)
9	5, 6	com2an 466	. . . . . . . . 9 (a v b) C (b ^ a)
10	8, 9	com2or 465	. . . . . . . 8 (a v b) C ((b ^ a_|_) v (b ^ a))
11	5	comcom2 175	. . . . . . . . 9 (a v b) C b_|_
12	5, 7	com2or 465	. . . . . . . . 9 (a v b) C (b v a_|_)
13	11, 12	com2an 466	. . . . . . . 8 (a v b) C (b_|_ ^ (b v a_|_))
14	10, 13	com2or 465	. . . . . . 7 (a v b) C (((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_)))
15	6, 11	com2an 466	. . . . . . . 8 (a v b) C (a ^ b_|_)
16	6, 11	com2or 465	. . . . . . . . 9 (a v b) C (a v b_|_)
17	7, 16	com2an 466	. . . . . . . 8 (a v b) C (a_|_ ^ (a v b_|_))
18	15, 17	com2or 465	. . . . . . 7 (a v b) C ((a ^ b_|_) v (a_|_ ^ (a v b_|_)))
19	14, 18	fh4 454	. . . . . 6 ((((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_))) v ((a v b) ^ ((a ^ b_|_) v (a_|_ ^ (a v b_|_))))) = (((((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_))) v (a v b)) ^ ((((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_))) v ((a ^ b_|_) v (a_|_ ^ (a v b_|_)))))
20		ax-a3 31	. . . . . . . 8 ((((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_))) v (a v b)) = (((b ^ a_|_) v (b ^ a)) v ((b_|_ ^ (b v a_|_)) v (a v b)))
21		or12 73	. . . . . . . . 9 (((b ^ a_|_) v (b ^ a)) v ((b_|_ ^ (b v a_|_)) v (a v b))) = ((b_|_ ^ (b v a_|_)) v (((b ^ a_|_) v (b ^ a)) v (a v b)))
22		ax-a3 31	. . . . . . . . . . . 12 (((b ^ a_|_) v (b ^ a)) v (a v b)) = ((b ^ a_|_) v ((b ^ a) v (a v b)))
23		ancom 68	. . . . . . . . . . . . . . . . 17 (b ^ a) = (a ^ b)
24		lea 152	. . . . . . . . . . . . . . . . 17 (a ^ b) =< a
25	23, 24	bltr 130	. . . . . . . . . . . . . . . 16 (b ^ a) =< a
26		leo 150	. . . . . . . . . . . . . . . 16 a =< (a v b)
27	25, 26	letr 129	. . . . . . . . . . . . . . 15 (b ^ a) =< (a v b)
28	27	df-le2 123	. . . . . . . . . . . . . 14 ((b ^ a) v (a v b)) = (a v b)
29	28	lor 66	. . . . . . . . . . . . 13 ((b ^ a_|_) v ((b ^ a) v (a v b))) = ((b ^ a_|_) v (a v b))
30		ax-a2 30	. . . . . . . . . . . . . 14 ((b ^ a_|_) v (a v b)) = ((a v b) v (b ^ a_|_))
31		ax-a3 31	. . . . . . . . . . . . . . 15 ((a v b) v (b ^ a_|_)) = (a v (b v (b ^ a_|_)))
32		a5b 112	. . . . . . . . . . . . . . . 16 (b v (b ^ a_|_)) = b
33	32	lor 66	. . . . . . . . . . . . . . 15 (a v (b v (b ^ a_|_))) = (a v b)
34	31, 33	ax-r2 35	. . . . . . . . . . . . . 14 ((a v b) v (b ^ a_|_)) = (a v b)
35	30, 34	ax-r2 35	. . . . . . . . . . . . 13 ((b ^ a_|_) v (a v b)) = (a v b)
36	29, 35	ax-r2 35	. . . . . . . . . . . 12 ((b ^ a_|_) v ((b ^ a) v (a v b))) = (a v b)
37	22, 36	ax-r2 35	. . . . . . . . . . 11 (((b ^ a_|_) v (b ^ a)) v (a v b)) = (a v b)
38	37	lor 66	. . . . . . . . . 10 ((b_|_ ^ (b v a_|_)) v (((b ^ a_|_) v (b ^ a)) v (a v b))) = ((b_|_ ^ (b v a_|_)) v (a v b))
39		ax-a2 30	. . . . . . . . . . 11 ((b_|_ ^ (b v a_|_)) v (a v b)) = ((a v b) v (b_|_ ^ (b v a_|_)))
40	5	comcom 435	. . . . . . . . . . . . . 14 b C (a v b)
41	40	comcom3 436	. . . . . . . . . . . . 13 b_|_ C (a v b)
42		comorr 176	. . . . . . . . . . . . . 14 b C (b v a_|_)
43	42	comcom3 436	. . . . . . . . . . . . 13 b_|_ C (b v a_|_)
44	41, 43	fh4 454	. . . . . . . . . . . 12 ((a v b) v (b_|_ ^ (b v a_|_))) = (((a v b) v b_|_) ^ ((a v b) v (b v a_|_)))
45		ax-a3 31	. . . . . . . . . . . . . . 15 ((a v b) v b_|_) = (a v (b v b_|_))
46		df-t 40	. . . . . . . . . . . . . . . . . 18 1 = (b v b_|_)
47	46	ax-r1 34	. . . . . . . . . . . . . . . . 17 (b v b_|_) = 1
48	47	lor 66	. . . . . . . . . . . . . . . 16 (a v (b v b_|_)) = (a v 1)
49		or1 96	. . . . . . . . . . . . . . . 16 (a v 1) = 1
50	48, 49	ax-r2 35	. . . . . . . . . . . . . . 15 (a v (b v b_|_)) = 1
51	45, 50	ax-r2 35	. . . . . . . . . . . . . 14 ((a v b) v b_|_) = 1
52		ax-a2 30	. . . . . . . . . . . . . . . 16 (a v b) = (b v a)
53	52	ax-r5 37	. . . . . . . . . . . . . . 15 ((a v b) v (b v a_|_)) = ((b v a) v (b v a_|_))
54		or4 77	. . . . . . . . . . . . . . . 16 ((b v a) v (b v a_|_)) = ((b v b) v (a v a_|_))
55		df-t 40	. . . . . . . . . . . . . . . . . . 19 1 = (a v a_|_)
56	55	ax-r1 34	. . . . . . . . . . . . . . . . . 18 (a v a_|_) = 1
57	56	lor 66	. . . . . . . . . . . . . . . . 17 ((b v b) v (a v a_|_)) = ((b v b) v 1)
58		or1 96	. . . . . . . . . . . . . . . . 17 ((b v b) v 1) = 1
59	57, 58	ax-r2 35	. . . . . . . . . . . . . . . 16 ((b v b) v (a v a_|_)) = 1
60	54, 59	ax-r2 35	. . . . . . . . . . . . . . 15 ((b v a) v (b v a_|_)) = 1
61	53, 60	ax-r2 35	. . . . . . . . . . . . . 14 ((a v b) v (b v a_|_)) = 1
62	51, 61	2an 72	. . . . . . . . . . . . 13 (((a v b) v b_|_) ^ ((a v b) v (b v a_|_))) = (1 ^ 1)
63		an1 98	. . . . . . . . . . . . 13 (1 ^ 1) = 1
64	62, 63	ax-r2 35	. . . . . . . . . . . 12 (((a v b) v b_|_) ^ ((a v b) v (b v a_|_))) = 1
65	44, 64	ax-r2 35	. . . . . . . . . . 11 ((a v b) v (b_|_ ^ (b v a_|_))) = 1
66	39, 65	ax-r2 35	. . . . . . . . . 10 ((b_|_ ^ (b v a_|_)) v (a v b)) = 1
67	38, 66	ax-r2 35	. . . . . . . . 9 ((b_|_ ^ (b v a_|_)) v (((b ^ a_|_) v (b ^ a)) v (a v b))) = 1
68	21, 67	ax-r2 35	. . . . . . . 8 (((b ^ a_|_) v (b ^ a)) v ((b_|_ ^ (b v a_|_)) v (a v b))) = 1
69	20, 68	ax-r2 35	. . . . . . 7 ((((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_))) v (a v b)) = 1
70		ax-a3 31	. . . . . . . 8 ((((b ^ a_|_) v (b ^ a)) v (b_|_ ^ (b v a_|_))) v ((a ^ b_|_) v (a_|_ ^ (a v b_|_)))) = (((b ^ a_|_) v (b ^ a)) v ((b_|_ ^ (b v a_|_)) v ((a ^ b_|_) v (a_|_ ^ (a v b_|_)))))
71		ax-a2 30	. . . . . . . . . . 11 ((b ^ a_|_) v (b ^ a)) = ((b ^ a) v (b ^ a_|_))
72		ancom 68	. . . . . . . . . . . 12 (b ^ a_|_) = (a_|_ ^ b)
73	72	lor 66	. . . . . . . . . . 11 ((b ^ a) v (b ^ a_|_)) = ((b ^ a) v (a_|_ ^ b))
74	71, 73	ax-r2 35	. . . . . . . . . 10 ((b ^ a_|_) v (b ^ a)) = ((b ^ a) v (a_|_ ^ b))
75		ax-a3 31	. . . . . . . . . . . 12 (((b_|_ ^ (b v a_|_)) v (a ^ b_|_)) v (a_|_ ^ (a v b_|_))) = ((b_|_ ^ (b v a_|_)) v ((a ^ b_|_) v (a_|_ ^ (a v b_|_))))
76	75	ax-r1 34	. . . . . . . . . . 11 ((b_|_