Theorem 3vded3 801

Description: A 3-variable theorem. Experiment with weak deduction theorem.

Hypotheses

Ref	Expression
3vded3.1	(c →0 C (a, c)) = 1
3vded3.2	(c →0 a) = 1
3vded3.3	(c →0 (a →0 b)) = 1

Assertion

Ref	Expression
3vded3	(c →0 b) = 1

Proof of Theorem 3vded3

Step	Hyp	Ref	Expression
1		df-i0 42	. 2 (c →0 b) = (c⊥ ∪ b)
2		ax-a3 31	. . 3 ((c⊥ ∪ a⊥ ) ∪ b) = (c⊥ ∪ (a⊥ ∪ b))
3		cmtrcom 182	. . . . . . . . . . . . . . . 16 C (c, a) = C (a, c)
4	3	lor 66	. . . . . . . . . . . . . . 15 (c⊥ ∪ C (c, a)) = (c⊥ ∪ C (a, c))
5		df-i0 42	. . . . . . . . . . . . . . 15 (c →0 C (c, a)) = (c⊥ ∪ C (c, a))
6		df-i0 42	. . . . . . . . . . . . . . 15 (c →0 C (a, c)) = (c⊥ ∪ C (a, c))
7	4, 5, 6	3tr1 60	. . . . . . . . . . . . . 14 (c →0 C (c, a)) = (c →0 C (a, c))
8		3vded3.1	. . . . . . . . . . . . . 14 (c →0 C (a, c)) = 1
9	7, 8	ax-r2 35	. . . . . . . . . . . . 13 (c →0 C (c, a)) = 1
10	9	i0cmtrcom 477	. . . . . . . . . . . 12 c C a
11	10	comcom4 437	. . . . . . . . . . 11 c⊥ C a⊥
12	11	comcom 435	. . . . . . . . . 10 a⊥ C c⊥
13		comid 179	. . . . . . . . . . 11 a C a
14	13	comcom3 436	. . . . . . . . . 10 a⊥ C a
15	12, 14	fh1 451	. . . . . . . . 9 (a⊥ ∩ (c⊥ ∪ a)) = ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ a))
16		df-i0 42	. . . . . . . . . . . 12 (c →0 a) = (c⊥ ∪ a)
17	16	ax-r1 34	. . . . . . . . . . 11 (c⊥ ∪ a) = (c →0 a)
18		3vded3.2	. . . . . . . . . . 11 (c →0 a) = 1
19	17, 18	ax-r2 35	. . . . . . . . . 10 (c⊥ ∪ a) = 1
20	19	lan 70	. . . . . . . . 9 (a⊥ ∩ (c⊥ ∪ a)) = (a⊥ ∩ 1)
21		dff 93	. . . . . . . . . . . . 13 0 = (a ∩ a⊥ )
22		ancom 68	. . . . . . . . . . . . 13 (a ∩ a⊥ ) = (a⊥ ∩ a)
23	21, 22	ax-r2 35	. . . . . . . . . . . 12 0 = (a⊥ ∩ a)
24	23	lor 66	. . . . . . . . . . 11 ((a⊥ ∩ c⊥ ) ∪ 0) = ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ a))
25	24	ax-r1 34	. . . . . . . . . 10 ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ a)) = ((a⊥ ∩ c⊥ ) ∪ 0)
26		or0 94	. . . . . . . . . 10 ((a⊥ ∩ c⊥ ) ∪ 0) = (a⊥ ∩ c⊥ )
27	25, 26	ax-r2 35	. . . . . . . . 9 ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ a)) = (a⊥ ∩ c⊥ )
28	15, 20, 27	3tr2 61	. . . . . . . 8 (a⊥ ∩ 1) = (a⊥ ∩ c⊥ )
29		an1 98	. . . . . . . 8 (a⊥ ∩ 1) = a⊥
30		ancom 68	. . . . . . . 8 (a⊥ ∩ c⊥ ) = (c⊥ ∩ a⊥ )
31	28, 29, 30	3tr2 61	. . . . . . 7 a⊥ = (c⊥ ∩ a⊥ )
32	31	lor 66	. . . . . 6 (c⊥ ∪ a⊥ ) = (c⊥ ∪ (c⊥ ∩ a⊥ ))
33		a5b 112	. . . . . 6 (c⊥ ∪ (c⊥ ∩ a⊥ )) = c⊥
34	32, 33	ax-r2 35	. . . . 5 (c⊥ ∪ a⊥ ) = c⊥
35	34	ax-r5 37	. . . 4 ((c⊥ ∪ a⊥ ) ∪ b) = (c⊥ ∪ b)
36	35	ax-r1 34	. . 3 (c⊥ ∪ b) = ((c⊥ ∪ a⊥ ) ∪ b)
37		df-i0 42	. . . 4 (c →0 (a →0 b)) = (c⊥ ∪ (a →0 b))
38		df-i0 42	. . . . 5 (a →0 b) = (a⊥ ∪ b)
39	38	lor 66	. . . 4 (c⊥ ∪ (a →0 b)) = (c⊥ ∪ (a⊥ ∪ b))
40	37, 39	ax-r2 35	. . 3 (c →0 (a →0 b)) = (c⊥ ∪ (a⊥ ∪ b))
41	2, 36, 40	3tr1 60	. 2 (c⊥ ∪ b) = (c →0 (a →0 b))
42		3vded3.3	. 2 (c →0 (a →0 b)) = 1
43	1, 41, 42	3tr 62	1 (c →0 b) = 1

Syntax hints:   = wb 1  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 9  0wf 10   →₀ wi0 12   C wcmtr 28

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-r3 421

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i0 42  df-le1 122  df-le2 123  df-c1 124  df-c2 125  df-cmtr 126

metamath.org