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)⊥ ∪ ((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)⊥ ∪ ((c →3 (c →3 a)) →3 (c →3 (c →3 b))))
3		lem4 493	. . . . . . 7 (c →3 (c →3 a)) = (c⊥ ∪ a)
4		lem4 493	. . . . . . 7 (c →3 (c →3 b)) = (c⊥ ∪ b)
5	3, 4	2i3 246	. . . . . 6 ((c →3 (c →3 a)) →3 (c →3 (c →3 b))) = ((c⊥ ∪ a) →3 (c⊥ ∪ b))
6	5	lor 66	. . . . 5 ((b →3 a)⊥ ∪ ((c →3 (c →3 a)) →3 (c →3 (c →3 b)))) = ((b →3 a)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ 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)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))
8	7	lor 66	. . 3 ((a →3 b)⊥ ∪ ((b →3 a) →3 ((b →3 a) →3 ((c →3 (c →3 a)) →3 (c →3 (c →3 b)))))) = ((a →3 b)⊥ ∪ ((b →3 a)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))))
9		oran3 85	. . . . . 6 ((a →3 b)⊥ ∪ (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)⊥ ∪ (b →3 a)⊥ ) = (a ≡ b)⊥
13	12	ax-r5 37	. . . 4 (((a →3 b)⊥ ∪ (b →3 a)⊥ ) ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))) = ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))
14		ax-a3 31	. . . 4 (((a →3 b)⊥ ∪ (b →3 a)⊥ ) ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))) = ((a →3 b)⊥ ∪ ((b →3 a)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))))
15		le1 138	. . . . 5 ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))) ≤ 1
16		ska4 415	. . . . . . . 8 ((a⊥ ≡ b⊥ )⊥ ∪ ((a⊥ ∩ c) ≡ (b⊥ ∩ c))) = 1
17	16	ax-r1 34	. . . . . . 7 1 = ((a⊥ ≡ b⊥ )⊥ ∪ ((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⊥ ∪ a) ≡ (c⊥ ∪ b)) = ((c⊥ ∪ a)⊥ ≡ (c⊥ ∪ b)⊥ )
21		ancom 68	. . . . . . . . . . . . 13 (a⊥ ∩ c) = (c ∩ a⊥ )
22		anor1 80	. . . . . . . . . . . . 13 (c ∩ a⊥ ) = (c⊥ ∪ a)⊥
23	21, 22	ax-r2 35	. . . . . . . . . . . 12 (a⊥ ∩ c) = (c⊥ ∪ a)⊥
24		ancom 68	. . . . . . . . . . . . 13 (b⊥ ∩ c) = (c ∩ b⊥ )
25		anor1 80	. . . . . . . . . . . . 13 (c ∩ b⊥ ) = (c⊥ ∪ b)⊥
26	24, 25	ax-r2 35	. . . . . . . . . . . 12 (b⊥ ∩ c) = (c⊥ ∪ b)⊥
27	23, 26	2bi 91	. . . . . . . . . . 11 ((a⊥ ∩ c) ≡ (b⊥ ∩ c)) = ((c⊥ ∪ a)⊥ ≡ (c⊥ ∪ b)⊥ )
28	27	ax-r1 34	. . . . . . . . . 10 ((c⊥ ∪ a)⊥ ≡ (c⊥ ∪ b)⊥ ) = ((a⊥ ∩ c) ≡ (b⊥ ∩ c))
29	20, 28	ax-r2 35	. . . . . . . . 9 ((c⊥ ∪ a) ≡ (c⊥ ∪ b)) = ((a⊥ ∩ c) ≡ (b⊥ ∩ c))
30	19, 29	2or 67	. . . . . . . 8 ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) ≡ (c⊥ ∪ b))) = ((a⊥ ≡ b⊥ )⊥ ∪ ((a⊥ ∩ c) ≡ (b⊥ ∩ c)))
31	30	ax-r1 34	. . . . . . 7 ((a⊥ ≡ b⊥ )⊥ ∪ ((a⊥ ∩ c) ≡ (b⊥ ∩ c))) = ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) ≡ (c⊥ ∪ b)))
32	17, 31	ax-r2 35	. . . . . 6 1 = ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) ≡ (c⊥ ∪ b)))
33		u3lembi 705	. . . . . . . . 9 (((c⊥ ∪ a) →3 (c⊥ ∪ b)) ∩ ((c⊥ ∪ b) →3 (c⊥ ∪ a))) = ((c⊥ ∪ a) ≡ (c⊥ ∪ b))
34	33	ax-r1 34	. . . . . . . 8 ((c⊥ ∪ a) ≡ (c⊥ ∪ b)) = (((c⊥ ∪ a) →3 (c⊥ ∪ b)) ∩ ((c⊥ ∪ b) →3 (c⊥ ∪ a)))
35		lea 152	. . . . . . . 8 (((c⊥ ∪ a) →3 (c⊥ ∪ b)) ∩ ((c⊥ ∪ b) →3 (c⊥ ∪ a))) ≤ ((c⊥ ∪ a) →3 (c⊥ ∪ b))
36	34, 35	bltr 130	. . . . . . 7 ((c⊥ ∪ a) ≡ (c⊥ ∪ b)) ≤ ((c⊥ ∪ a) →3 (c⊥ ∪ b))
37	36	lelor 158	. . . . . 6 ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) ≡ (c⊥ ∪ b))) ≤ ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))
38	32, 37	bltr 130	. . . . 5 1 ≤ ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))
39	15, 38	lebi 137	. . . 4 ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))) = 1
40	13, 14, 39	3tr2 61	. . 3 ((a →3 b)⊥ ∪ ((b →3 a)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))) = 1
41	8, 40	ax-r2 35	. 2 ((a →3 b)⊥ ∪ ((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   ∪ wo 6   ∩ wa 7  1wt 9   →₃ 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