Theorem elimcons2 851

Description: Consequent elimination law.

Hypotheses

Ref	Expression
elimcons2.1	(a ->1 c) = (b ->1 c)
elimcons2.2	(a ^ (c ^ (b ->1 c))) =< (b v (c_|_ v (a ->1 c)_|_))

Assertion

Ref	Expression
elimcons2	a =< b

Proof of Theorem elimcons2

Step	Hyp	Ref	Expression
1		elimcons2.1	. 2 (a ->1 c) = (b ->1 c)
2		elimcons2.2	. . 3 (a ^ (c ^ (b ->1 c))) =< (b v (c_|_ v (a ->1 c)_|_))
3	1	ax-r1 34	. . . . . . 7 (b ->1 c) = (a ->1 c)
4		df-i1 43	. . . . . . 7 (a ->1 c) = (a_|_ v (a ^ c))
5	3, 4	ax-r2 35	. . . . . 6 (b ->1 c) = (a_|_ v (a ^ c))
6	5	lan 70	. . . . 5 (c ^ (b ->1 c)) = (c ^ (a_|_ v (a ^ c)))
7	6	lan 70	. . . 4 (a ^ (c ^ (b ->1 c))) = (a ^ (c ^ (a_|_ v (a ^ c))))
8		anass 69	. . . . 5 ((a ^ c) ^ (a_|_ v (a ^ c))) = (a ^ (c ^ (a_|_ v (a ^ c))))
9	8	ax-r1 34	. . . 4 (a ^ (c ^ (a_|_ v (a ^ c)))) = ((a ^ c) ^ (a_|_ v (a ^ c)))
10		leor 151	. . . . 5 (a ^ c) =< (a_|_ v (a ^ c))
11	10	df2le2 128	. . . 4 ((a ^ c) ^ (a_|_ v (a ^ c))) = (a ^ c)
12	7, 9, 11	3tr 62	. . 3 (a ^ (c ^ (b ->1 c))) = (a ^ c)
13	1	ax-r4 36	. . . . . . . 8 (a ->1 c)_|_ = (b ->1 c)_|_
14		ud1lem0c 269	. . . . . . . 8 (b ->1 c)_|_ = (b ^ (b_|_ v c_|_))
15	13, 14	ax-r2 35	. . . . . . 7 (a ->1 c)_|_ = (b ^ (b_|_ v c_|_))
16	15	lor 66	. . . . . 6 (c_|_ v (a ->1 c)_|_) = (c_|_ v (b ^ (b_|_ v c_|_)))
17		ax-a2 30	. . . . . 6 (c_|_ v (b ^ (b_|_ v c_|_))) = ((b ^ (b_|_ v c_|_)) v c_|_)
18	16, 17	ax-r2 35	. . . . 5 (c_|_ v (a ->1 c)_|_) = ((b ^ (b_|_ v c_|_)) v c_|_)
19	18	lor 66	. . . 4 (b v (c_|_ v (a ->1 c)_|_)) = (b v ((b ^ (b_|_ v c_|_)) v c_|_))
20		ax-a3 31	. . . . 5 ((b v (b ^ (b_|_ v c_|_))) v c_|_) = (b v ((b ^ (b_|_ v c_|_)) v c_|_))
21	20	ax-r1 34	. . . 4 (b v ((b ^ (b_|_ v c_|_)) v c_|_)) = ((b v (b ^ (b_|_ v c_|_))) v c_|_)
22		ax-a2 30	. . . . . 6 (b v (b ^ (b_|_ v c_|_))) = ((b ^ (b_|_ v c_|_)) v b)
23		lea 152	. . . . . . 7 (b ^ (b_|_ v c_|_)) =< b
24	23	df-le2 123	. . . . . 6 ((b ^ (b_|_ v c_|_)) v b) = b
25	22, 24	ax-r2 35	. . . . 5 (b v (b ^ (b_|_ v c_|_))) = b
26	25	ax-r5 37	. . . 4 ((b v (b ^ (b_|_ v c_|_))) v c_|_) = (b v c_|_)
27	19, 21, 26	3tr 62	. . 3 (b v (c_|_ v (a ->1 c)_|_)) = (b v c_|_)
28	2, 12, 27	le3tr2 133	. 2 (a ^ c) =< (b v c_|_)
29	1, 28	elimcons 850	1 a =< b

Syntax hints:   = wb 1   =< wle 2  _|_wn 4   v wo 6   ^ wa 7   ->1 wi1 13

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

metamath.org