Theorem i3bi 478

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 81	. . . . . . 7 (b_|_ ^ a) = (b v a_|_)_|_
2		lea 152	. . . . . . . . . . . . 13 (a_|_ ^ b) =< a_|_
3		leo 150	. . . . . . . . . . . . . 14 a_|_ =< (a_|_ v b)
4		ax-a2 30	. . . . . . . . . . . . . 14 (a_|_ v b) = (b v a_|_)
5	3, 4	lbtr 131	. . . . . . . . . . . . 13 a_|_ =< (b v a_|_)
6	2, 5	letr 129	. . . . . . . . . . . 12 (a_|_ ^ b) =< (b v a_|_)
7		lea 152	. . . . . . . . . . . . 13 ((a_|_ v b) ^ a) =< (a_|_ v b)
8		ancom 68	. . . . . . . . . . . . 13 (a ^ (a_|_ v b)) = ((a_|_ v b) ^ a)
9		ax-a2 30	. . . . . . . . . . . . 13 (b v a_|_) = (a_|_ v b)
10	7, 8, 9	le3tr1 132	. . . . . . . . . . . 12 (a ^ (a_|_ v b)) =< (b v a_|_)
11	6, 10	le2or 160	. . . . . . . . . . 11 ((a_|_ ^ b) v (a ^ (a_|_ v b))) =< ((b v a_|_) v (b v a_|_))
12		oridm 102	. . . . . . . . . . 11 ((b v a_|_) v (b v a_|_)) = (b v a_|_)
13	11, 12	lbtr 131	. . . . . . . . . 10 ((a_|_ ^ b) v (a ^ (a_|_ v b))) =< (b v a_|_)
14	13	lecom 172	. . . . . . . . 9 ((a_|_ ^ b) v (a ^ (a_|_ v b))) C (b v a_|_)
15	14	comcom2 175	. . . . . . . 8 ((a_|_ ^ b) v (a ^ (a_|_ v b))) C (b v a_|_)_|_
16	15	comcom 435	. . . . . . 7 (b v a_|_)_|_ C ((a_|_ ^ b) v (a ^ (a_|_ v b)))
17	1, 16	bctr 173	. . . . . 6 (b_|_ ^ a) C ((a_|_ ^ b) v (a ^ (a_|_ v b)))
18		lea 152	. . . . . . . . . . 11 (b ^ (b_|_ v a)) =< b
19		leo 150	. . . . . . . . . . 11 b =< (b v a_|_)
20	18, 19	letr 129	. . . . . . . . . 10 (b ^ (b_|_ v a)) =< (b v a_|_)
21	20	lecom 172	. . . . . . . . 9 (b ^ (b_|_ v a)) C (b v a_|_)
22	21	comcom2 175	. . . . . . . 8 (b ^ (b_|_ v a)) C (b v a_|_)_|_
23	22	comcom 435	. . . . . . 7 (b v a_|_)_|_ C (b ^ (b_|_ v a))
24	1, 23	bctr 173	. . . . . 6 (b_|_ ^ a) C (b ^ (b_|_ v a))
25	17, 24	fh2 452	. . . . 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 68	. . . . . . . 8 (((a_|_ ^ b) v (a ^ (a_|_ v b))) ^ (b_|_ ^ a)) = ((b_|_ ^ a) ^ ((a_|_ ^ b) v (a ^ (a_|_ v b))))
27		lea 152	. . . . . . . . . . . . . 14 (b_|_ ^ a) =< b_|_
28		leo 150	. . . . . . . . . . . . . 14 b_|_ =< (b_|_ v a)
29	27, 28	letr 129	. . . . . . . . . . . . 13 (b_|_ ^ a) =< (b_|_ v a)
30	29	lecom 172	. . . . . . . . . . . 12 (b_|_ ^ a) C (b_|_ v a)
31	30	comcom2 175	. . . . . . . . . . 11 (b_|_ ^ a) C (b_|_ v a)_|_
32		ancom 68	. . . . . . . . . . . . 13 (a_|_ ^ b) = (b ^ a_|_)
33		anor1 80	. . . . . . . . . . . . 13 (b ^ a_|_) = (b_|_ v a)_|_
34	32, 33	ax-r2 35	. . . . . . . . . . . 12 (a_|_ ^ b) = (b_|_ v a)_|_
35	34	ax-r1 34	. . . . . . . . . . 11 (b_|_ v a)_|_ = (a_|_ ^ b)
36	31, 35	cbtr 174	. . . . . . . . . 10 (b_|_ ^ a) C (a_|_ ^ b)
37		ancom 68	. . . . . . . . . . . 12 (b_|_ ^ a) = (a ^ b_|_)
38		anor1 80	. . . . . . . . . . . 12 (a ^ b_|_) = (a_|_ v b)_|_
39	37, 38	ax-r2 35	. . . . . . . . . . 11 (b_|_ ^ a) = (a_|_ v b)_|_
40	8, 7	bltr 130	. . . . . . . . . . . . . 14 (a ^ (a_|_ v b)) =< (a_|_ v b)
41	40	lecom 172	. . . . . . . . . . . . 13 (a ^ (a_|_ v b)) C (a_|_ v b)
42	41	comcom2 175	. . . . . . . . . . . 12 (a ^ (a_|_ v b)) C (a_|_ v b)_|_
43	42	comcom 435	. . . . . . . . . . 11 (a_|_ v b)_|_ C (a ^ (a_|_ v b))
44	39, 43	bctr 173	. . . . . . . . . 10 (b_|_ ^ a) C (a ^ (a_|_ v b))
45	36, 44	fh1 451	. . . . . . . . 9 ((b_|_ ^ a) ^ ((a_|_ ^ b) v (a ^ (a_|_ v b)))) = (((b_|_ ^ a) ^ (a_|_ ^ b)) v ((b_|_ ^ a) ^ (a ^ (a_|_ v b))))
46	37	ran 71	. . . . . . . . . . . 12 ((b_|_ ^ a) ^ (a_|_ ^ b)) = ((a ^ b_|_) ^ (a_|_ ^ b))
47		an4 78	. . . . . . . . . . . . 13 ((a ^ b_|_) ^ (a_|_ ^ b)) = ((a ^ a_|_) ^ (b_|_ ^ b))
48		dff 93	. . . . . . . . . . . . . . . 16 0 = (a ^ a_|_)
49		dff 93	. . . . . . . . . . . . . . . . 17 0 = (b ^ b_|_)
50		ancom 68	. . . . . . . . . . . . . . . . 17 (b ^ b_|_) = (b_|_ ^ b)
51	49, 50	ax-r2 35	. . . . . . . . . . . . . . . 16 0 = (b_|_ ^ b)
52	48, 51	2an 72	. . . . . . . . . . . . . . 15 (0 ^ 0) = ((a ^ a_|_) ^ (b_|_ ^ b))
53	52	ax-r1 34	. . . . . . . . . . . . . 14 ((a ^ a_|_) ^ (b_|_ ^ b)) = (0 ^ 0)
54		anidm 103	. . . . . . . . . . . . . 14 (0 ^ 0) = 0
55	53, 54	ax-r2 35	. . . . . . . . . . . . 13 ((a ^ a_|_) ^ (b_|_ ^ b)) = 0
56	47, 55	ax-r2 35	. . . . . . . . . . . 12 ((a ^ b_|_) ^ (a_|_ ^ b)) = 0
57	46, 56	ax-r2 35	. . . . . . . . . . 11 ((b_|_ ^ a) ^ (a_|_ ^ b)) = 0
58		an12 74	. . . . . . . . . . . 12 ((b_|_ ^ a) ^ (a ^ (a_|_ v b))) = (a ^ ((b_|_ ^ a) ^ (a_|_ v b)))
59		dff 93	. . . . . . . . . . . . . . . 16 0 = ((b_|_ ^ a) ^ (b_|_ ^ a)_|_)
60	1	con2 64	. . . . . . . . . . . . . . . . . 18 (b_|_ ^ a)_|_ = (b v a_|_)
61	60, 9	ax-r2 35	. . . . . . . . . . . . . . . . 17 (b_|_ ^ a)_|_ = (a_|_ v b)
62	61	lan 70	. . . . . . . . . . . . . . . 16 ((b_|_ ^ a) ^ (b_|_ ^ a)_|_) = ((b_|_ ^ a) ^ (a_|_ v b))
63	59, 62	ax-r2 35	. . . . . . . . . . . . . . 15 0 = ((b_|_ ^ a) ^ (a_|_ v b))
64	63	lan 70	. . . . . . . . . . . . . 14 (a ^ 0) = (a ^ ((b_|_ ^ a) ^ (a_|_ v b)))
65	64	ax-r1 34	. . . . . . . . . . . . 13 (a ^ ((b_|_ ^ a) ^ (a_|_ v b))) = (a ^ 0)
66		an0 100	. . . . . . . . . . . . 13 (a ^ 0) = 0
67	65, 66	ax-r2 35	. . . . . . . . . . . 12 (a ^ ((b_|_ ^ a) ^ (a_|_ v b))) = 0
68	58, 67	ax-r2 35	. . . . . . . . . . 11 ((b_|_ ^ a) ^ (a ^ (a_|_ v b))) = 0
69	57, 68	2or 67	. . . . . . . . . 10 (((b_|_ ^ a) ^ (a_|_ ^ b)) v ((b_|_ ^ a) ^ (a ^ (a_|_ v b)))) = (0 v 0)
70		oridm 102	. . . . . . . . . 10 (0 v 0) = 0
71	69, 70	ax-r2 35	. . . . . . . . 9 (((b_|_ ^ a) ^ (a_|_ ^ b)) v ((b_|_ ^ a) ^ (a ^ (a_|_ v b)))) = 0
72	45, 71	ax-r2 35	. . . . . . . 8 ((b_|_ ^ a) ^ ((a_|_ ^ b) v (a ^ (a_|_ v b)))) = 0
73	26, 72	ax-r2 35	. . . . . . 7 (((a_|_ ^ b) v (a ^ (a_|_ v b))) ^ (b_|_ ^ a)) = 0
74		ancom 68	. . . . . . . 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 68	. . . . . . . . . . . . . . 15 (b ^ (b_|_ v a)) = ((b_|_ v a) ^ b)
76		lea 152	. . . . . . . . . . . . . . 15 ((b_|_ v a) ^ b) =< (b_|_ v a)
77	75, 76	bltr 130	. . . . . . . . . . . . . 14 (b ^ (b_|_ v a)) =< (b_|_ v a)
78	77	lecom 172	. . . . . . . . . . . . 13 (b ^ (b_|_ v a)) C (b_|_ v a)
79	78	comcom2 175	. . . . . . . . . . . 12 (b ^ (b_|_ v a)) C (b_|_ v a)_|_
80	79	comcom 435	. . . . . . . . . . 11 (b_|_ v a)_|_ C (b ^ (b_|_ v a))
81	34, 80	bctr 173	. . . . . . . . . 10 (a_|_ ^ b) C (b ^ (b_|_ v a))
82		anor2 81	. . . . . . . . . . 11 (a_|_ ^ b) = (a v b_|_)_|_
83		lea 152	. . . . . . . . . . . . . . 15 (a ^ (a_|_ v b)) =< a
84		leo 150	. . . . . . . . . . . . . . 15 a =< (a v b_|_)
85	83, 84	letr 129	. . . . . . . . . . . . . 14 (a ^ (a_|_ v b)) =< (a v b_|_)
86	85	lecom 172	. . . . . . . . . . . . 13 (a ^ (a_|_ v b)) C (a v b_|_)
87	86	comcom2 175	. . . . . . . . . . . 12 (a ^ (a_|_ v b)) C (a v b_|_)_|_
88	87	comcom 435	. . . . . . . . . . 11 (a v b_|_)_|_ C (a ^ (a_|_ v b))
89	82, 88	bctr 173	. . . . . . . . . 10 (a_|_ ^ b) C (a ^ (a_|_ v b))
90	81, 89	fh2 452	. . . . . . . . 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 30	. . . . . . . . . 10 (((b ^ (b_|_ v a)) ^ (a_|_ ^ b)) v ((b ^ (b_|_ v a)) ^ (a ^ (a_|_ v b)))) = (((b ^ (b_|_ v a)) ^ (a ^ (a_|_ v b))) v ((b ^ (b_|_ v a)) ^ (a_|_