Theorem 3vded21 799

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

Hypotheses

Ref	Expression
3vded21.1	c =< ((a ->0 b) ->0 (c ->2 b))
3vded21.2	c =< (a ->0 b)

Assertion

Ref	Expression
3vded21	c =< b

Proof of Theorem 3vded21

Step	Hyp	Ref	Expression
1		3vded21.2	. . . . . . 7 c =< (a ->0 b)
2		df-i0 42	. . . . . . 7 (a ->0 b) = (a_|_ v b)
3	1, 2	lbtr 131	. . . . . 6 c =< (a_|_ v b)
4		3vded21.1	. . . . . . 7 c =< ((a ->0 b) ->0 (c ->2 b))
5		df-i0 42	. . . . . . . 8 ((a ->0 b) ->0 (c ->2 b)) = ((a ->0 b)_|_ v (c ->2 b))
6	2	ax-r4 36	. . . . . . . . 9 (a ->0 b)_|_ = (a_|_ v b)_|_
7		df-i2 44	. . . . . . . . . 10 (c ->2 b) = (b v (c_|_ ^ b_|_))
8		anor3 82	. . . . . . . . . . 11 (c_|_ ^ b_|_) = (c v b)_|_
9	8	lor 66	. . . . . . . . . 10 (b v (c_|_ ^ b_|_)) = (b v (c v b)_|_)
10	7, 9	ax-r2 35	. . . . . . . . 9 (c ->2 b) = (b v (c v b)_|_)
11	6, 10	2or 67	. . . . . . . 8 ((a ->0 b)_|_ v (c ->2 b)) = ((a_|_ v b)_|_ v (b v (c v b)_|_))
12		ax-a2 30	. . . . . . . 8 ((a_|_ v b)_|_ v (b v (c v b)_|_)) = ((b v (c v b)_|_) v (a_|_ v b)_|_)
13	5, 11, 12	3tr 62	. . . . . . 7 ((a ->0 b) ->0 (c ->2 b)) = ((b v (c v b)_|_) v (a_|_ v b)_|_)
14	4, 13	lbtr 131	. . . . . 6 c =< ((b v (c v b)_|_) v (a_|_ v b)_|_)
15	3, 14	ler2an 165	. . . . 5 c =< ((a_|_ v b) ^ ((b v (c v b)_|_) v (a_|_ v b)_|_))
16		comor2 444	. . . . . . . 8 (a_|_ v b) C b
17	3	leror 144	. . . . . . . . . . . 12 (c v b) =< ((a_|_ v b) v b)
18		ax-a3 31	. . . . . . . . . . . . 13 ((a_|_ v b) v b) = (a_|_ v (b v b))
19		oridm 102	. . . . . . . . . . . . . 14 (b v b) = b
20	19	lor 66	. . . . . . . . . . . . 13 (a_|_ v (b v b)) = (a_|_ v b)
21	18, 20	ax-r2 35	. . . . . . . . . . . 12 ((a_|_ v b) v b) = (a_|_ v b)
22	17, 21	lbtr 131	. . . . . . . . . . 11 (c v b) =< (a_|_ v b)
23	22	lecom 172	. . . . . . . . . 10 (c v b) C (a_|_ v b)
24	23	comcom 435	. . . . . . . . 9 (a_|_ v b) C (c v b)
25	24	comcom2 175	. . . . . . . 8 (a_|_ v b) C (c v b)_|_
26	16, 25	com2or 465	. . . . . . 7 (a_|_ v b) C (b v (c v b)_|_)
27		comid 179	. . . . . . . 8 (a_|_ v b) C (a_|_ v b)
28	27	comcom2 175	. . . . . . 7 (a_|_ v b) C (a_|_ v b)_|_
29	26, 28	fh1 451	. . . . . 6 ((a_|_ v b) ^ ((b v (c v b)_|_) v (a_|_ v b)_|_)) = (((a_|_ v b) ^ (b v (c v b)_|_)) v ((a_|_ v b) ^ (a_|_ v b)_|_))
30		or0 94	. . . . . . 7 ((((a_|_ v b) ^ b) v ((a_|_ v b) ^ (c v b)_|_)) v 0) = (((a_|_ v b) ^ b) v ((a_|_ v b) ^ (c v b)_|_))
31	16, 25	fh1 451	. . . . . . . . 9 ((a_|_ v b) ^ (b v (c v b)_|_)) = (((a_|_ v b) ^ b) v ((a_|_ v b) ^ (c v b)_|_))
32	31	ax-r1 34	. . . . . . . 8 (((a_|_ v b) ^ b) v ((a_|_ v b) ^ (c v b)_|_)) = ((a_|_ v b) ^ (b v (c v b)_|_))
33		dff 93	. . . . . . . 8 0 = ((a_|_ v b) ^ (a_|_ v b)_|_)
34	32, 33	2or 67	. . . . . . 7 ((((a_|_ v b) ^ b) v ((a_|_ v b) ^ (c v b)_|_)) v 0) = (((a_|_ v b) ^ (b v (c v b)_|_)) v ((a_|_ v b) ^ (a_|_ v b)_|_))
35		ax-a2 30	. . . . . . . . . 10 (a_|_ v b) = (b v a_|_)
36	35	ran 71	. . . . . . . . 9 ((a_|_ v b) ^ b) = ((b v a_|_) ^ b)
37		ancom 68	. . . . . . . . 9 ((b v a_|_) ^ b) = (b ^ (b v a_|_))
38		a5c 113	. . . . . . . . 9 (b ^ (b v a_|_)) = b
39	36, 37, 38	3tr 62	. . . . . . . 8 ((a_|_ v b) ^ b) = b
40	39	ax-r5 37	. . . . . . 7 (((a_|_ v b) ^ b) v ((a_|_ v b) ^ (c v b)_|_)) = (b v ((a_|_ v b) ^ (c v b)_|_))
41	30, 34, 40	3tr2 61	. . . . . 6 (((a_|_ v b) ^ (b v (c v b)_|_)) v ((a_|_ v b) ^ (a_|_ v b)_|_)) = (b v ((a_|_ v b) ^ (c v b)_|_))
42	29, 41	ax-r2 35	. . . . 5 ((a_|_ v b) ^ ((b v (c v b)_|_) v (a_|_ v b)_|_)) = (b v ((a_|_ v b) ^ (c v b)_|_))
43	15, 42	lbtr 131	. . . 4 c =< (b v ((a_|_ v b) ^ (c v b)_|_))
44	43	leran 145	. . 3 (c ^ (c v b)) =< ((b v ((a_|_ v b) ^ (c v b)_|_)) ^ (c v b))
45		a5c 113	. . 3 (c ^ (c v b)) = c
46		comor2 444	. . . . 5 (c v b) C b
47		comid 179	. . . . . . 7 (c v b) C (c v b)
48	47	comcom2 175	. . . . . 6 (c v b) C (c v b)_|_
49	23, 48	com2an 466	. . . . 5 (c v b) C ((a_|_ v b) ^ (c v b)_|_)
50	46, 49	fh1r 455	. . . 4 ((b v ((a_|_ v b) ^ (c v b)_|_)) ^ (c v b)) = ((b ^ (c v b)) v (((a_|_ v b) ^ (c v b)_|_) ^ (c v b)))
51		ax-a2 30	. . . . . . 7 (c v b) = (b v c)
52	51	lan 70	. . . . . 6 (b ^ (c v b)) = (b ^ (b v c))
53		a5c 113	. . . . . 6 (b ^ (b v c)) = b
54	52, 53	ax-r2 35	. . . . 5 (b ^ (c v b)) = b
55		an32 76	. . . . . 6 (((a_|_ v b) ^ (c v b)_|_) ^ (c v b)) = (((a_|_ v b) ^ (c v b)) ^ (c v b)_|_)
56		anass 69	. . . . . 6 (((a_|_ v b) ^ (c v b)) ^ (c v b)_|_) = ((a_|_ v b) ^ ((c v b) ^ (c v b)_|_))
57		dff 93	. . . . . . . . 9 0 = ((c v b) ^ (c v b)_|_)
58	57	lan 70	. . . . . . . 8 ((a_|_ v b) ^ 0) = ((a_|_ v b) ^ ((c v b) ^ (c v b)_|_))
59	58	ax-r1 34	. . . . . . 7 ((a_|_ v b) ^ ((c v b) ^ (c v b)_|_)) = ((a_|_ v b) ^ 0)
60		an0 100	. . . . . . 7 ((a_|_ v b) ^ 0) = 0
61	59, 60	ax-r2 35	. . . . . 6 ((a_|_ v b) ^ ((c v b) ^ (c v b)_|_)) = 0
62	55, 56, 61	3tr 62	. . . . 5 (((a_|_ v b) ^ (c v b)_|_) ^ (c v b)) = 0
63	54, 62	2or 67	. . . 4 ((b ^ (c v b)) v (((a_|_ v b) ^ (c v b)_|_) ^ (c v b))) = (b v 0)
64	50, 63	ax-r2 35	. . 3 ((b v ((a_|_ v b) ^ (c v b)_|_)) ^ (c v b)) = (b v 0)
65	44, 45, 64	le3tr2 133	. 2 c =< (b v 0)
66		or0 94	. 2 (b v 0) = b
67	65, 66	lbtr 131	1 c =< b

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7  0wf 10   ->0 wi0 12   ->2 wi2 14

This theorem is referenced by:  3vded22 800

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-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org