Theorem u3lemax4 796

Description: Possible axiom for Kalmbach implication system. (Contributed by NM, 21-Jan-1998.)

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 511	. 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 511	. . . . 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 511	. . . . . . 7 (c →3 (c →3 a)) = (c⊥ ∪ a)
4		lem4 511	. . . . . . 7 (c →3 (c →3 b)) = (c⊥ ∪ b)
5	3, 4	2i3 254	. . . . . 6 ((c →3 (c →3 a)) →3 (c →3 (c →3 b))) = ((c⊥ ∪ a) →3 (c⊥ ∪ b))
6	5	lor 70	. . . . 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 36	. . . 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 70	. . 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 93	. . . . . 6 ((a →3 b)⊥ ∪ (b →3 a)⊥ ) = ((a →3 b) ∩ (b →3 a))⊥
10		u3lembi 723	. . . . . . 7 ((a →3 b) ∩ (b →3 a)) = (a ≡ b)
11	10	ax-r4 37	. . . . . 6 ((a →3 b) ∩ (b →3 a))⊥ = (a ≡ b)⊥
12	9, 11	ax-r2 36	. . . . 5 ((a →3 b)⊥ ∪ (b →3 a)⊥ ) = (a ≡ b)⊥
13	12	ax-r5 38	. . . 4 (((a →3 b)⊥ ∪ (b →3 a)⊥ ) ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))) = ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))
14		ax-a3 32	. . . 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 146	. . . . 5 ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))) ≤ 1
16		ska4 433	. . . . . . . 8 ((a⊥ ≡ b⊥ )⊥ ∪ ((a⊥ ∩ c) ≡ (b⊥ ∩ c))) = 1
17	16	ax-r1 35	. . . . . . 7 1 = ((a⊥ ≡ b⊥ )⊥ ∪ ((a⊥ ∩ c) ≡ (b⊥ ∩ c)))
18		conb 122	. . . . . . . . . 10 (a ≡ b) = (a⊥ ≡ b⊥ )
19	18	ax-r4 37	. . . . . . . . 9 (a ≡ b)⊥ = (a⊥ ≡ b⊥ )⊥
20		conb 122	. . . . . . . . . 10 ((c⊥ ∪ a) ≡ (c⊥ ∪ b)) = ((c⊥ ∪ a)⊥ ≡ (c⊥ ∪ b)⊥ )
21		ancom 74	. . . . . . . . . . . . 13 (a⊥ ∩ c) = (c ∩ a⊥ )
22		anor1 88	. . . . . . . . . . . . 13 (c ∩ a⊥ ) = (c⊥ ∪ a)⊥
23	21, 22	ax-r2 36	. . . . . . . . . . . 12 (a⊥ ∩ c) = (c⊥ ∪ a)⊥
24		ancom 74	. . . . . . . . . . . . 13 (b⊥ ∩ c) = (c ∩ b⊥ )
25		anor1 88	. . . . . . . . . . . . 13 (c ∩ b⊥ ) = (c⊥ ∪ b)⊥
26	24, 25	ax-r2 36	. . . . . . . . . . . 12 (b⊥ ∩ c) = (c⊥ ∪ b)⊥
27	23, 26	2bi 99	. . . . . . . . . . 11 ((a⊥ ∩ c) ≡ (b⊥ ∩ c)) = ((c⊥ ∪ a)⊥ ≡ (c⊥ ∪ b)⊥ )
28	27	ax-r1 35	. . . . . . . . . 10 ((c⊥ ∪ a)⊥ ≡ (c⊥ ∪ b)⊥ ) = ((a⊥ ∩ c) ≡ (b⊥ ∩ c))
29	20, 28	ax-r2 36	. . . . . . . . 9 ((c⊥ ∪ a) ≡ (c⊥ ∪ b)) = ((a⊥ ∩ c) ≡ (b⊥ ∩ c))
30	19, 29	2or 72	. . . . . . . 8 ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) ≡ (c⊥ ∪ b))) = ((a⊥ ≡ b⊥ )⊥ ∪ ((a⊥ ∩ c) ≡ (b⊥ ∩ c)))
31	30	ax-r1 35	. . . . . . 7 ((a⊥ ≡ b⊥ )⊥ ∪ ((a⊥ ∩ c) ≡ (b⊥ ∩ c))) = ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) ≡ (c⊥ ∪ b)))
32	17, 31	ax-r2 36	. . . . . 6 1 = ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) ≡ (c⊥ ∪ b)))
33		u3lembi 723	. . . . . . . . 9 (((c⊥ ∪ a) →3 (c⊥ ∪ b)) ∩ ((c⊥ ∪ b) →3 (c⊥ ∪ a))) = ((c⊥ ∪ a) ≡ (c⊥ ∪ b))
34	33	ax-r1 35	. . . . . . . 8 ((c⊥ ∪ a) ≡ (c⊥ ∪ b)) = (((c⊥ ∪ a) →3 (c⊥ ∪ b)) ∩ ((c⊥ ∪ b) →3 (c⊥ ∪ a)))
35		lea 160	. . . . . . . 8 (((c⊥ ∪ a) →3 (c⊥ ∪ b)) ∩ ((c⊥ ∪ b) →3 (c⊥ ∪ a))) ≤ ((c⊥ ∪ a) →3 (c⊥ ∪ b))
36	34, 35	bltr 138	. . . . . . 7 ((c⊥ ∪ a) ≡ (c⊥ ∪ b)) ≤ ((c⊥ ∪ a) →3 (c⊥ ∪ b))
37	36	lelor 166	. . . . . 6 ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) ≡ (c⊥ ∪ b))) ≤ ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))
38	32, 37	bltr 138	. . . . 5 1 ≤ ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))
39	15, 38	lebi 145	. . . 4 ((a ≡ b)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b))) = 1
40	13, 14, 39	3tr2 64	. . 3 ((a →3 b)⊥ ∪ ((b →3 a)⊥ ∪ ((c⊥ ∪ a) →3 (c⊥ ∪ b)))) = 1
41	8, 40	ax-r2 36	. 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 36	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 8   →₃ wi3 14

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-wom 361  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-i2 45  df-i3 46  df-le 129  df-le1 130  df-le2 131  df-c1 132  df-c2 133  df-cmtr 134

This theorem is referenced by: (None)