Theorem elimcons 850

Description: Consequent elimination law.

Hypotheses

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

Assertion

Ref	Expression
elimcons	a =< b

Proof of Theorem elimcons

Step	Hyp	Ref	Expression
1		df-t 40	. . . . . . . 8 1 = (a v a_|_)
2		elimcons.1	. . . . . . . . . 10 (a ->1 c) = (b ->1 c)
3		elimcons.2	. . . . . . . . . 10 (a ^ c) =< (b v c_|_)
4	2, 3	elimconslem 849	. . . . . . . . 9 a =< (b v c_|_)
5	4	leror 144	. . . . . . . 8 (a v a_|_) =< ((b v c_|_) v a_|_)
6	1, 5	bltr 130	. . . . . . 7 1 =< ((b v c_|_) v a_|_)
7	6	lelan 159	. . . . . 6 (b_|_ ^ 1) =< (b_|_ ^ ((b v c_|_) v a_|_))
8		an1 98	. . . . . 6 (b_|_ ^ 1) = b_|_
9		comor1 443	. . . . . . . 8 (b v c_|_) C b
10	9	comcom2 175	. . . . . . 7 (b v c_|_) C b_|_
11	4	lecom 172	. . . . . . . . 9 a C (b v c_|_)
12	11	comcom3 436	. . . . . . . 8 a_|_ C (b v c_|_)
13	12	comcom 435	. . . . . . 7 (b v c_|_) C a_|_
14	10, 13	fh2 452	. . . . . 6 (b_|_ ^ ((b v c_|_) v a_|_)) = ((b_|_ ^ (b v c_|_)) v (b_|_ ^ a_|_))
15	7, 8, 14	le3tr2 133	. . . . 5 b_|_ =< ((b_|_ ^ (b v c_|_)) v (b_|_ ^ a_|_))
16	2	negant 834	. . . . . . . . . . 11 (a_|_ ->1 c) = (b_|_ ->1 c)
17		df-i1 43	. . . . . . . . . . 11 (a_|_ ->1 c) = (a_|__|_ v (a_|_ ^ c))
18		df-i1 43	. . . . . . . . . . 11 (b_|_ ->1 c) = (b_|__|_ v (b_|_ ^ c))
19	16, 17, 18	3tr2 61	. . . . . . . . . 10 (a_|__|_ v (a_|_ ^ c)) = (b_|__|_ v (b_|_ ^ c))
20		anor2 81	. . . . . . . . . . 11 (a_|_ ^ c) = (a v c_|_)_|_
21	20	lor 66	. . . . . . . . . 10 (a_|__|_ v (a_|_ ^ c)) = (a_|__|_ v (a v c_|_)_|_)
22		anor2 81	. . . . . . . . . . 11 (b_|_ ^ c) = (b v c_|_)_|_
23	22	lor 66	. . . . . . . . . 10 (b_|__|_ v (b_|_ ^ c)) = (b_|__|_ v (b v c_|_)_|_)
24	19, 21, 23	3tr2 61	. . . . . . . . 9 (a_|__|_ v (a v c_|_)_|_) = (b_|__|_ v (b v c_|_)_|_)
25	24	ax-r1 34	. . . . . . . 8 (b_|__|_ v (b v c_|_)_|_) = (a_|__|_ v (a v c_|_)_|_)
26	25	ax-r4 36	. . . . . . 7 (b_|__|_ v (b v c_|_)_|_)_|_ = (a_|__|_ v (a v c_|_)_|_)_|_
27		df-a 39	. . . . . . 7 (b_|_ ^ (b v c_|_)) = (b_|__|_ v (b v c_|_)_|_)_|_
28		df-a 39	. . . . . . 7 (a_|_ ^ (a v c_|_)) = (a_|__|_ v (a v c_|_)_|_)_|_
29	26, 27, 28	3tr1 60	. . . . . 6 (b_|_ ^ (b v c_|_)) = (a_|_ ^ (a v c_|_))
30	29	ax-r5 37	. . . . 5 ((b_|_ ^ (b v c_|_)) v (b_|_ ^ a_|_)) = ((a_|_ ^ (a v c_|_)) v (b_|_ ^ a_|_))
31	15, 30	lbtr 131	. . . 4 b_|_ =< ((a_|_ ^ (a v c_|_)) v (b_|_ ^ a_|_))
32		lear 153	. . . . 5 (b_|_ ^ a_|_) =< a_|_
33	32	lelor 158	. . . 4 ((a_|_ ^ (a v c_|_)) v (b_|_ ^ a_|_)) =< ((a_|_ ^ (a v c_|_)) v a_|_)
34	31, 33	letr 129	. . 3 b_|_ =< ((a_|_ ^ (a v c_|_)) v a_|_)
35		lea 152	. . . 4 (a_|_ ^ (a v c_|_)) =< a_|_
36	35	df-le2 123	. . 3 ((a_|_ ^ (a v c_|_)) v a_|_) = a_|_
37	34, 36	lbtr 131	. 2 b_|_ =< a_|_
38	37	lecon1 147	1 a =< b

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

This theorem is referenced by:  elimcons2 851

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