Theorem 3vded22 800

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

Hypotheses

Ref	Expression
3vded22.1	c =< ( C (a, b) v C (c, b))
3vded22.2	c =< a
3vded22.3	c =< (a ->0 b)

Assertion

Ref	Expression
3vded22	c =< b

Proof of Theorem 3vded22

Step	Hyp	Ref	Expression
1		3vded22.1	. . . 4 c =< ( C (a, b) v C (c, b))
2		df-cmtr 126	. . . . . . 7 C (a, b) = (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (a_|_ ^ b_|_)))
3		or4 77	. . . . . . 7 (((a ^ b) v (a ^ b_|_)) v ((a_|_ ^ b) v (a_|_ ^ b_|_))) = (((a ^ b) v (a_|_ ^ b)) v ((a ^ b_|_) v (a_|_ ^ b_|_)))
4	2, 3	ax-r2 35	. . . . . 6 C (a, b) = (((a ^ b) v (a_|_ ^ b)) v ((a ^ b_|_) v (a_|_ ^ b_|_)))
5		lear 153	. . . . . . . 8 (a ^ b) =< b
6		lear 153	. . . . . . . 8 (a_|_ ^ b) =< b
7	5, 6	lel2or 162	. . . . . . 7 ((a ^ b) v (a_|_ ^ b)) =< b
8		3vded22.2	. . . . . . . . . 10 c =< a
9	8	lecon 146	. . . . . . . . 9 a_|_ =< c_|_
10	9	leran 145	. . . . . . . 8 (a_|_ ^ b_|_) =< (c_|_ ^ b_|_)
11	10	lelor 158	. . . . . . 7 ((a ^ b_|_) v (a_|_ ^ b_|_)) =< ((a ^ b_|_) v (c_|_ ^ b_|_))
12	7, 11	le2or 160	. . . . . 6 (((a ^ b) v (a_|_ ^ b)) v ((a ^ b_|_) v (a_|_ ^ b_|_))) =< (b v ((a ^ b_|_) v (c_|_ ^ b_|_)))
13	4, 12	bltr 130	. . . . 5 C (a, b) =< (b v ((a ^ b_|_) v (c_|_ ^ b_|_)))
14		df-cmtr 126	. . . . . . 7 C (c, b) = (((c ^ b) v (c ^ b_|_)) v ((c_|_ ^ b) v (c_|_ ^ b_|_)))
15		or4 77	. . . . . . 7 (((c ^ b) v (c ^ b_|_)) v ((c_|_ ^ b) v (c_|_ ^ b_|_))) = (((c ^ b) v (c_|_ ^ b)) v ((c ^ b_|_) v (c_|_ ^ b_|_)))
16	14, 15	ax-r2 35	. . . . . 6 C (c, b) = (((c ^ b) v (c_|_ ^ b)) v ((c ^ b_|_) v (c_|_ ^ b_|_)))
17		lear 153	. . . . . . . 8 (c ^ b) =< b
18		lear 153	. . . . . . . 8 (c_|_ ^ b) =< b
19	17, 18	lel2or 162	. . . . . . 7 ((c ^ b) v (c_|_ ^ b)) =< b
20	8	leran 145	. . . . . . . 8 (c ^ b_|_) =< (a ^ b_|_)
21	20	leror 144	. . . . . . 7 ((c ^ b_|_) v (c_|_ ^ b_|_)) =< ((a ^ b_|_) v (c_|_ ^ b_|_))
22	19, 21	le2or 160	. . . . . 6 (((c ^ b) v (c_|_ ^ b)) v ((c ^ b_|_) v (c_|_ ^ b_|_))) =< (b v ((a ^ b_|_) v (c_|_ ^ b_|_)))
23	16, 22	bltr 130	. . . . 5 C (c, b) =< (b v ((a ^ b_|_) v (c_|_ ^ b_|_)))
24	13, 23	le2or 160	. . . 4 ( C (a, b) v C (c, b)) =< ((b v ((a ^ b_|_) v (c_|_ ^ b_|_))) v (b v ((a ^ b_|_) v (c_|_ ^ b_|_))))
25	1, 24	letr 129	. . 3 c =< ((b v ((a ^ b_|_) v (c_|_ ^ b_|_))) v (b v ((a ^ b_|_) v (c_|_ ^ b_|_))))
26		df-i0 42	. . . . 5 ((a ->0 b) ->0 (c ->2 b)) = ((a ->0 b)_|_ v (c ->2 b))
27		or12 73	. . . . . 6 ((a ^ b_|_) v (b v (c_|_ ^ b_|_))) = (b v ((a ^ b_|_) v (c_|_ ^ b_|_)))
28		df-i0 42	. . . . . . . . 9 (a ->0 b) = (a_|_ v b)
29	28	ax-r4 36	. . . . . . . 8 (a ->0 b)_|_ = (a_|_ v b)_|_
30		anor1 80	. . . . . . . . 9 (a ^ b_|_) = (a_|_ v b)_|_
31	30	ax-r1 34	. . . . . . . 8 (a_|_ v b)_|_ = (a ^ b_|_)
32	29, 31	ax-r2 35	. . . . . . 7 (a ->0 b)_|_ = (a ^ b_|_)
33		df-i2 44	. . . . . . 7 (c ->2 b) = (b v (c_|_ ^ b_|_))
34	32, 33	2or 67	. . . . . 6 ((a ->0 b)_|_ v (c ->2 b)) = ((a ^ b_|_) v (b v (c_|_ ^ b_|_)))
35		oridm 102	. . . . . 6 ((b v ((a ^ b_|_) v (c_|_ ^ b_|_))) v (b v ((a ^ b_|_) v (c_|_ ^ b_|_)))) = (b v ((a ^ b_|_) v (c_|_ ^ b_|_)))
36	27, 34, 35	3tr1 60	. . . . 5 ((a ->0 b)_|_ v (c ->2 b)) = ((b v ((a ^ b_|_) v (c_|_ ^ b_|_))) v (b v ((a ^ b_|_) v (c_|_ ^ b_|_))))
37	26, 36	ax-r2 35	. . . 4 ((a ->0 b) ->0 (c ->2 b)) = ((b v ((a ^ b_|_) v (c_|_ ^ b_|_))) v (b v ((a ^ b_|_) v (c_|_ ^ b_|_))))
38	37	ax-r1 34	. . 3 ((b v ((a ^ b_|_) v (c_|_ ^ b_|_))) v (b v ((a ^ b_|_) v (c_|_ ^ b_|_)))) = ((a ->0 b) ->0 (c ->2 b))
39	25, 38	lbtr 131	. 2 c =< ((a ->0 b) ->0 (c ->2 b))
40		3vded22.3	. 2 c =< (a ->0 b)
41	39, 40	3vded21 799	1 c =< b

Syntax hints:   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->0 wi0 12   ->2 wi2 14   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-i2 44  df-le1 122  df-le2 123  df-c1 124  df-c2 125  df-cmtr 126

metamath.org