Theorem 3vded3 819

Description: A 3-variable theorem. Experiment with weak deduction theorem. (Contributed by NM, 24-Jan-1999.)

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 43	. 2 (c →0 b) = (c⊥ ∪ b)
2		ax-a3 32	. . 3 ((c⊥ ∪ a⊥ ) ∪ b) = (c⊥ ∪ (a⊥ ∪ b))
3		cmtrcom 190	. . . . . . . . . . . . . . . 16 C (c, a) = C (a, c)
4	3	lor 70	. . . . . . . . . . . . . . 15 (c⊥ ∪ C (c, a)) = (c⊥ ∪ C (a, c))
5		df-i0 43	. . . . . . . . . . . . . . 15 (c →0 C (c, a)) = (c⊥ ∪ C (c, a))
6		df-i0 43	. . . . . . . . . . . . . . 15 (c →0 C (a, c)) = (c⊥ ∪ C (a, c))
7	4, 5, 6	3tr1 63	. . . . . . . . . . . . . 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 36	. . . . . . . . . . . . 13 (c →0 C (c, a)) = 1
10	9	i0cmtrcom 495	. . . . . . . . . . . 12 c C a
11	10	comcom4 455	. . . . . . . . . . 11 c⊥ C a⊥
12	11	comcom 453	. . . . . . . . . 10 a⊥ C c⊥
13		comid 187	. . . . . . . . . . 11 a C a
14	13	comcom3 454	. . . . . . . . . 10 a⊥ C a
15	12, 14	fh1 469	. . . . . . . . 9 (a⊥ ∩ (c⊥ ∪ a)) = ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ a))
16		df-i0 43	. . . . . . . . . . . 12 (c →0 a) = (c⊥ ∪ a)
17	16	ax-r1 35	. . . . . . . . . . 11 (c⊥ ∪ a) = (c →0 a)
18		3vded3.2	. . . . . . . . . . 11 (c →0 a) = 1
19	17, 18	ax-r2 36	. . . . . . . . . 10 (c⊥ ∪ a) = 1
20	19	lan 77	. . . . . . . . 9 (a⊥ ∩ (c⊥ ∪ a)) = (a⊥ ∩ 1)
21		dff 101	. . . . . . . . . . . . 13 0 = (a ∩ a⊥ )
22		ancom 74	. . . . . . . . . . . . 13 (a ∩ a⊥ ) = (a⊥ ∩ a)
23	21, 22	ax-r2 36	. . . . . . . . . . . 12 0 = (a⊥ ∩ a)
24	23	lor 70	. . . . . . . . . . 11 ((a⊥ ∩ c⊥ ) ∪ 0) = ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ a))
25	24	ax-r1 35	. . . . . . . . . 10 ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ a)) = ((a⊥ ∩ c⊥ ) ∪ 0)
26		or0 102	. . . . . . . . . 10 ((a⊥ ∩ c⊥ ) ∪ 0) = (a⊥ ∩ c⊥ )
27	25, 26	ax-r2 36	. . . . . . . . 9 ((a⊥ ∩ c⊥ ) ∪ (a⊥ ∩ a)) = (a⊥ ∩ c⊥ )
28	15, 20, 27	3tr2 64	. . . . . . . 8 (a⊥ ∩ 1) = (a⊥ ∩ c⊥ )
29		an1 106	. . . . . . . 8 (a⊥ ∩ 1) = a⊥
30		ancom 74	. . . . . . . 8 (a⊥ ∩ c⊥ ) = (c⊥ ∩ a⊥ )
31	28, 29, 30	3tr2 64	. . . . . . 7 a⊥ = (c⊥ ∩ a⊥ )
32	31	lor 70	. . . . . 6 (c⊥ ∪ a⊥ ) = (c⊥ ∪ (c⊥ ∩ a⊥ ))
33		orabs 120	. . . . . 6 (c⊥ ∪ (c⊥ ∩ a⊥ )) = c⊥
34	32, 33	ax-r2 36	. . . . 5 (c⊥ ∪ a⊥ ) = c⊥
35	34	ax-r5 38	. . . 4 ((c⊥ ∪ a⊥ ) ∪ b) = (c⊥ ∪ b)
36	35	ax-r1 35	. . 3 (c⊥ ∪ b) = ((c⊥ ∪ a⊥ ) ∪ b)
37		df-i0 43	. . . 4 (c →0 (a →0 b)) = (c⊥ ∪ (a →0 b))
38		df-i0 43	. . . . 5 (a →0 b) = (a⊥ ∪ b)
39	38	lor 70	. . . 4 (c⊥ ∪ (a →0 b)) = (c⊥ ∪ (a⊥ ∪ b))
40	37, 39	ax-r2 36	. . 3 (c →0 (a →0 b)) = (c⊥ ∪ (a⊥ ∪ b))
41	2, 36, 40	3tr1 63	. 2 (c⊥ ∪ b) = (c →0 (a →0 b))
42		3vded3.3	. 2 (c →0 (a →0 b)) = 1
43	1, 41, 42	3tr 65	1 (c →0 b) = 1

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

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

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i0 43  df-le1 130  df-le2 131  df-c1 132  df-c2 133  df-cmtr 134

This theorem is referenced by: (None)