Theorem i3bi 496

Description: Kalmbach implication and biconditional.

Assertion

Ref	Expression
i3bi	((a ->3 b) ^ (b ->3 a)) = (a == b)

Proof of Theorem i3bi

Step	Hyp	Ref	Expression
1		anor2 89	. . . . . . 7 (b' ^ a) = (b v a')'
2		lea 160	. . . . . . . . . . . . 13 (a' ^ b) =< a'
3		leo 158	. . . . . . . . . . . . . 14 a' =< (a' v b)
4		ax-a2 31	. . . . . . . . . . . . . 14 (a' v b) = (b v a')
5	3, 4	lbtr 139	. . . . . . . . . . . . 13 a' =< (b v a')
6	2, 5	letr 137	. . . . . . . . . . . 12 (a' ^ b) =< (b v a')
7		lea 160	. . . . . . . . . . . . 13 ((a' v b) ^ a) =< (a' v b)
8		ancom 74	. . . . . . . . . . . . 13 (a ^ (a' v b)) = ((a' v b) ^ a)
9		ax-a2 31	. . . . . . . . . . . . 13 (b v a') = (a' v b)
10	7, 8, 9	le3tr1 140	. . . . . . . . . . . 12 (a ^ (a' v b)) =< (b v a')
11	6, 10	le2or 168	. . . . . . . . . . 11 ((a' ^ b) v (a ^ (a' v b))) =< ((b v a') v (b v a'))
12		oridm 110	. . . . . . . . . . 11 ((b v a') v (b v a')) = (b v a')
13	11, 12	lbtr 139	. . . . . . . . . 10 ((a' ^ b) v (a ^ (a' v b))) =< (b v a')
14	13	lecom 180	. . . . . . . . 9 ((a' ^ b) v (a ^ (a' v b))) C (b v a')
15	14	comcom2 183	. . . . . . . 8 ((a' ^ b) v (a ^ (a' v b))) C (b v a')'
16	15	comcom 453	. . . . . . 7 (b v a')' C ((a' ^ b) v (a ^ (a' v b)))
17	1, 16	bctr 181	. . . . . 6 (b' ^ a) C ((a' ^ b) v (a ^ (a' v b)))
18		lea 160	. . . . . . . . . . 11 (b ^ (b' v a)) =< b
19		leo 158	. . . . . . . . . . 11 b =< (b v a')
20	18, 19	letr 137	. . . . . . . . . 10 (b ^ (b' v a)) =< (b v a')
21	20	lecom 180	. . . . . . . . 9 (b ^ (b' v a)) C (b v a')
22	21	comcom2 183	. . . . . . . 8 (b ^ (b' v a)) C (b v a')'
23	22	comcom 453	. . . . . . 7 (b v a')' C (b ^ (b' v a))
24	1, 23	bctr 181	. . . . . 6 (b' ^ a) C (b ^ (b' v a))
25	17, 24	fh2 470	. . . . 5 (((a' ^ b) v (a ^ (a' v b))) ^ ((b' ^ a) v (b ^ (b' v a)))) = ((((a' ^ b) v (a ^ (a' v b))) ^ (b' ^ a)) v (((a' ^ b) v (a ^ (a' v b))) ^ (b ^ (b' v a))))
26		ancom 74	. . . . . . . 8 (((a' ^ b) v (a ^ (a' v b))) ^ (b' ^ a)) = ((b' ^ a) ^ ((a' ^ b) v (a ^ (a' v b))))
27		lea 160	. . . . . . . . . . . . . 14 (b' ^ a) =< b'
28		leo 158	. . . . . . . . . . . . . 14 b' =< (b' v a)
29	27, 28	letr 137	. . . . . . . . . . . . 13 (b' ^ a) =< (b' v a)
30	29	lecom 180	. . . . . . . . . . . 12 (b' ^ a) C (b' v a)
31	30	comcom2 183	. . . . . . . . . . 11 (b' ^ a) C (b' v a)'
32		ancom 74	. . . . . . . . . . . . 13 (a' ^ b) = (b ^ a')
33		anor1 88	. . . . . . . . . . . . 13 (b ^ a') = (b' v a)'
34	32, 33	ax-r2 36	. . . . . . . . . . . 12 (a' ^ b) = (b' v a)'
35	34	ax-r1 35	. . . . . . . . . . 11 (b' v a)' = (a' ^ b)
36	31, 35	cbtr 182	. . . . . . . . . 10 (b' ^ a) C (a' ^ b)
37		ancom 74	. . . . . . . . . . . 12 (b' ^ a) = (a ^ b')
38		anor1 88	. . . . . . . . . . . 12 (a ^ b') = (a' v b)'
39	37, 38	ax-r2 36	. . . . . . . . . . 11 (b' ^ a) = (a' v b)'
40	8, 7	bltr 138	. . . . . . . . . . . . . 14 (a ^ (a' v b)) =< (a' v b)
41	40	lecom 180	. . . . . . . . . . . . 13 (a ^ (a' v b)) C (a' v b)
42	41	comcom2 183	. . . . . . . . . . . 12 (a ^ (a' v b)) C (a' v b)'
43	42	comcom 453	. . . . . . . . . . 11 (a' v b)' C (a ^ (a' v b))
44	39, 43	bctr 181	. . . . . . . . . 10 (b' ^ a) C (a ^ (a' v b))
45	36, 44	fh1 469	. . . . . . . . 9 ((b' ^ a) ^ ((a' ^ b) v (a ^ (a' v b)))) = (((b' ^ a) ^ (a' ^ b)) v ((b' ^ a) ^ (a ^ (a' v b))))
46	37	ran 78	. . . . . . . . . . . 12 ((b' ^ a) ^ (a' ^ b)) = ((a ^ b') ^ (a' ^ b))
47		an4 86	. . . . . . . . . . . . 13 ((a ^ b') ^ (a' ^ b)) = ((a ^ a') ^ (b' ^ b))
48		dff 101	. . . . . . . . . . . . . . . 16 0 = (a ^ a')
49		dff 101	. . . . . . . . . . . . . . . . 17 0 = (b ^ b')
50		ancom 74	. . . . . . . . . . . . . . . . 17 (b ^ b') = (b' ^ b)
51	49, 50	ax-r2 36	. . . . . . . . . . . . . . . 16 0 = (b' ^ b)
52	48, 51	2an 79	. . . . . . . . . . . . . . 15 (0 ^ 0) = ((a ^ a') ^ (b' ^ b))
53	52	ax-r1 35	. . . . . . . . . . . . . 14 ((a ^ a') ^ (b' ^ b)) = (0 ^ 0)
54		anidm 111	. . . . . . . . . . . . . 14 (0 ^ 0) = 0
55	53, 54	ax-r2 36	. . . . . . . . . . . . 13 ((a ^ a') ^ (b' ^ b)) = 0
56	47, 55	ax-r2 36	. . . . . . . . . . . 12 ((a ^ b') ^ (a' ^ b)) = 0
57	46, 56	ax-r2 36	. . . . . . . . . . 11 ((b' ^ a) ^ (a' ^ b)) = 0
58		an12 81	. . . . . . . . . . . 12 ((b' ^ a) ^ (a ^ (a' v b))) = (a ^ ((b' ^ a) ^ (a' v b)))
59		dff 101	. . . . . . . . . . . . . . . 16 0 = ((b' ^ a) ^ (b' ^ a)')
60	1	con2 67	. . . . . . . . . . . . . . . . . 18 (b' ^ a)' = (b v a')
61	60, 9	ax-r2 36	. . . . . . . . . . . . . . . . 17 (b' ^ a)' = (a' v b)
62	61	lan 77	. . . . . . . . . . . . . . . 16 ((b' ^ a) ^ (b' ^ a)') = ((b' ^ a) ^ (a' v b))
63	59, 62	ax-r2 36	. . . . . . . . . . . . . . 15 0 = ((b' ^ a) ^ (a' v b))
64	63	lan 77	. . . . . . . . . . . . . 14 (a ^ 0) = (a ^ ((b' ^ a) ^ (a' v b)))
65	64	ax-r1 35	. . . . . . . . . . . . 13 (a ^ ((b' ^ a) ^ (a' v b))) = (a ^ 0)
66		an0 108	. . . . . . . . . . . . 13 (a ^ 0) = 0
67	65, 66	ax-r2 36	. . . . . . . . . . . 12 (a ^ ((b' ^ a) ^ (a' v b))) = 0
68	58, 67	ax-r2 36	. . . . . . . . . . 11 ((b' ^ a) ^ (a ^ (a' v b))) = 0
69	57, 68	2or 72	. . . . . . . . . 10 (((b' ^ a) ^ (a' ^ b)) v ((b' ^ a) ^ (a ^ (a' v b)))) = (0 v 0)
70		oridm 110	. . . . . . . . . 10 (0 v 0) = 0
71	69, 70	ax-r2 36	. . . . . . . . 9 (((b' ^ a) ^ (a' ^ b)) v ((b' ^ a) ^ (a ^ (a' v b)))) = 0
72	45, 71	ax-r2 36	. . . . . . . 8 ((b' ^ a) ^ ((a' ^ b) v (a ^ (a' v b)))) = 0
73	26, 72	ax-r2 36	. . . . . . 7 (((a' ^ b) v (a ^ (a' v b))) ^ (b' ^ a)) = 0
74		ancom 74	. . . . . . . 8 (((a' ^ b) v (a ^ (a' v b))) ^ (b ^ (b' v a))) = ((b ^ (b' v a)) ^ ((a' ^ b) v (a ^ (a' v b))))
75		ancom 74	. . . . . . . . . . . . . . 15 (b ^ (b' v a)) = ((b' v a) ^ b)
76		lea 160	. . . . . . . . . . . . . . 15 ((b' v a) ^ b) =< (b' v a)
77	75, 76	bltr 138	. . . . . . . . . . . . . 14 (b ^ (b' v a)) =< (b' v a)
78	77	lecom 180	. . . . . . . . . . . . 13 (b ^ (b' v a)) C (b' v a)
79	78	comcom2 183	. . . . . . . . . . . 12 (b ^ (b' v a)) C (b' v a)'
80	79	comcom 453	. . . . . . . . . . 11 (b' v a)' C (b ^ (b' v a))
81	34, 80	bctr 181	. . . . . . . . . 10 (a' ^ b) C (b ^ (b' v a))
82		anor2 89	. . . . . . . . . . 11 (a' ^ b) = (a v b')'
83		lea 160	. . . . . . . . . . . . . . 15 (a ^ (a' v b)) =< a
84		leo 158	. . . . . . . . . . . . . . 15 a =< (a v b')
85	83, 84	letr 137	. . . . . . . . . . . . . 14 (a ^ (a' v b)) =< (a v b')
86	85	lecom 180	. . . . . . . . . . . . 13 (a ^ (a' v b)) C (a v b')
87	86	comcom2 183	. . . . . . . . . . . 12 (a ^ (a' v b)) C (a v b')'
88	87	comcom 453	. . . . . . . . . . 11 (a v b')' C (a ^ (a' v b))
89	82, 88	bctr 181	. . . . . . . . . 10 (a' ^ b) C (a ^ (a' v b))
90	81, 89	fh2 470	. . . . . . . . 9 ((b ^ (b' v a)) ^ ((a' ^ b) v (a ^ (a' v b)))) = (((b ^ (b' v a)) ^ (a' ^ b)) v ((b ^ (b' v a)) ^ (a ^ (a' v b))))
91		ax-a2 31	. . . . . . . . . 10 (((b ^ (b' v a)) ^ (a' ^ b)) v ((b ^ (b' v a