Theorem i3con 551

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 502	. . . . 5 (a ->3 b)' = ((a v b) ^ ((a ^ b') v (a' ^ (a v b'))))
2		i3n1 249	. . . . 5 (b' ->3 a') = (((b ^ a') v (b ^ a)) v (b' ^ (b v a')))
3	1, 2	2or 72	. . . 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 31	. . . . 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 462	. . . . . . . . . 10 (a v b) C b
6		comor1 461	. . . . . . . . . . 11 (a v b) C a
7	6	comcom2 183	. . . . . . . . . 10 (a v b) C a'
8	5, 7	com2an 484	. . . . . . . . 9 (a v b) C (b ^ a')
9	5, 6	com2an 484	. . . . . . . . 9 (a v b) C (b ^ a)
10	8, 9	com2or 483	. . . . . . . 8 (a v b) C ((b ^ a') v (b ^ a))
11	5	comcom2 183	. . . . . . . . 9 (a v b) C b'
12	5, 7	com2or 483	. . . . . . . . 9 (a v b) C (b v a')
13	11, 12	com2an 484	. . . . . . . 8 (a v b) C (b' ^ (b v a'))
14	10, 13	com2or 483	. . . . . . 7 (a v b) C (((b ^ a') v (b ^ a)) v (b' ^ (b v a')))
15	6, 11	com2an 484	. . . . . . . 8 (a v b) C (a ^ b')
16	6, 11	com2or 483	. . . . . . . . 9 (a v b) C (a v b')
17	7, 16	com2an 484	. . . . . . . 8 (a v b) C (a' ^ (a v b'))
18	15, 17	com2or 483	. . . . . . 7 (a v b) C ((a ^ b') v (a' ^ (a v b')))
19	14, 18	fh4 472	. . . . . 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 32	. . . . . . . 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 80	. . . . . . . . 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 32	. . . . . . . . . . . 12 (((b ^ a') v (b ^ a)) v (a v b)) = ((b ^ a') v ((b ^ a) v (a v b)))
23		ancom 74	. . . . . . . . . . . . . . . . 17 (b ^ a) = (a ^ b)
24		lea 160	. . . . . . . . . . . . . . . . 17 (a ^ b) =< a
25	23, 24	bltr 138	. . . . . . . . . . . . . . . 16 (b ^ a) =< a
26		leo 158	. . . . . . . . . . . . . . . 16 a =< (a v b)
27	25, 26	letr 137	. . . . . . . . . . . . . . 15 (b ^ a) =< (a v b)
28	27	df-le2 131	. . . . . . . . . . . . . 14 ((b ^ a) v (a v b)) = (a v b)
29	28	lor 70	. . . . . . . . . . . . 13 ((b ^ a') v ((b ^ a) v (a v b))) = ((b ^ a') v (a v b))
30		ax-a2 31	. . . . . . . . . . . . . 14 ((b ^ a') v (a v b)) = ((a v b) v (b ^ a'))
31		ax-a3 32	. . . . . . . . . . . . . . 15 ((a v b) v (b ^ a')) = (a v (b v (b ^ a')))
32		a5b 120	. . . . . . . . . . . . . . . 16 (b v (b ^ a')) = b
33	32	lor 70	. . . . . . . . . . . . . . 15 (a v (b v (b ^ a'))) = (a v b)
34	31, 33	ax-r2 36	. . . . . . . . . . . . . 14 ((a v b) v (b ^ a')) = (a v b)
35	30, 34	ax-r2 36	. . . . . . . . . . . . 13 ((b ^ a') v (a v b)) = (a v b)
36	29, 35	ax-r2 36	. . . . . . . . . . . 12 ((b ^ a') v ((b ^ a) v (a v b))) = (a v b)
37	22, 36	ax-r2 36	. . . . . . . . . . 11 (((b ^ a') v (b ^ a)) v (a v b)) = (a v b)
38	37	lor 70	. . . . . . . . . 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 31	. . . . . . . . . . 11 ((b' ^ (b v a')) v (a v b)) = ((a v b) v (b' ^ (b v a')))
40	5	comcom 453	. . . . . . . . . . . . . 14 b C (a v b)
41	40	comcom3 454	. . . . . . . . . . . . 13 b' C (a v b)
42		comorr 184	. . . . . . . . . . . . . 14 b C (b v a')
43	42	comcom3 454	. . . . . . . . . . . . 13 b' C (b v a')
44	41, 43	fh4 472	. . . . . . . . . . . 12 ((a v b) v (b' ^ (b v a'))) = (((a v b) v b') ^ ((a v b) v (b v a')))
45		ax-a3 32	. . . . . . . . . . . . . . 15 ((a v b) v b') = (a v (b v b'))
46		df-t 41	. . . . . . . . . . . . . . . . . 18 1 = (b v b')
47	46	ax-r1 35	. . . . . . . . . . . . . . . . 17 (b v b') = 1
48	47	lor 70	. . . . . . . . . . . . . . . 16 (a v (b v b')) = (a v 1)
49		or1 104	. . . . . . . . . . . . . . . 16 (a v 1) = 1
50	48, 49	ax-r2 36	. . . . . . . . . . . . . . 15 (a v (b v b')) = 1
51	45, 50	ax-r2 36	. . . . . . . . . . . . . 14 ((a v b) v b') = 1
52		ax-a2 31	. . . . . . . . . . . . . . . 16 (a v b) = (b v a)
53	52	ax-r5 38	. . . . . . . . . . . . . . 15 ((a v b) v (b v a')) = ((b v a) v (b v a'))
54		or4 84	. . . . . . . . . . . . . . . 16 ((b v a) v (b v a')) = ((b v b) v (a v a'))
55		df-t 41	. . . . . . . . . . . . . . . . . . 19 1 = (a v a')
56	55	ax-r1 35	. . . . . . . . . . . . . . . . . 18 (a v a') = 1
57	56	lor 70	. . . . . . . . . . . . . . . . 17 ((b v b) v (a v a')) = ((b v b) v 1)
58		or1 104	. . . . . . . . . . . . . . . . 17 ((b v b) v 1) = 1
59	57, 58	ax-r2 36	. . . . . . . . . . . . . . . 16 ((b v b) v (a v a')) = 1
60	54, 59	ax-r2 36	. . . . . . . . . . . . . . 15 ((b v a) v (b v a')) = 1
61	53, 60	ax-r2 36	. . . . . . . . . . . . . 14 ((a v b) v (b v a')) = 1
62	51, 61	2an 79	. . . . . . . . . . . . 13 (((a v b) v b') ^ ((a v b) v (b v a'))) = (1 ^ 1)
63		an1 106	. . . . . . . . . . . . 13 (1 ^ 1) = 1
64	62, 63	ax-r2 36	. . . . . . . . . . . 12 (((a v b) v b') ^ ((a v b) v (b v a'))) = 1
65	44, 64	ax-r2 36	. . . . . . . . . . 11 ((a v b) v (b' ^ (b v a'))) = 1
66	39, 65	ax-r2 36	. . . . . . . . . 10 ((b' ^ (b v a')) v (a v b)) = 1
67	38, 66	ax-r2 36	. . . . . . . . 9 ((b' ^ (b v a')) v (((b ^ a') v (b ^ a)) v (a v b))) = 1
68	21, 67	ax-r2 36	. . . . . . . 8 (((b ^ a') v (b ^ a)) v ((b' ^ (b v a')) v (a v b))) = 1
69	20, 68	ax-r2 36	. . . . . . 7 ((((b ^ a') v (b ^ a)) v (b' ^ (b v a'))) v (a v b)) = 1
70		ax-a3 32	. . . . . . . 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 31	. . . . . . . . . . 11 ((b ^ a') v (b ^ a)) = ((b ^ a) v (b ^ a'))
72		ancom 74	. . . . . . . . . . . 12 (b ^ a') = (a' ^ b)
73	72	lor 70	. . . . . . . . . . 11 ((b ^ a) v (b ^ a')) = ((b ^ a) v (a' ^ b))
74	71, 73	ax-r2 36	. . . . . . . . . 10 ((b ^ a') v (b ^ a)) = ((b ^ a) v (a' ^ b))
75		ax-a3 32	. . . . . . . . . . . 12 (((b' ^ (b v a')) v (a ^ b')) v (a' ^ (a v b')