Theorem elimconslem 849

Description: Lemma for consequent elimination law.

Hypotheses

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

Assertion

Ref	Expression
elimconslem	a =< (b v c_|_)

Proof of Theorem elimconslem

Step	Hyp	Ref	Expression
1		df-t 40	. . . . . . 7 1 = ((b v c_|_) v (b v c_|_)_|_)
2		elimcons.2	. . . . . . . . . 10 (a ^ c) =< (b v c_|_)
3	2	lecon 146	. . . . . . . . 9 (b v c_|_)_|_ =< (a ^ c)_|_
4		oran3 85	. . . . . . . . . 10 (a_|_ v c_|_) = (a ^ c)_|_
5	4	ax-r1 34	. . . . . . . . 9 (a ^ c)_|_ = (a_|_ v c_|_)
6	3, 5	lbtr 131	. . . . . . . 8 (b v c_|_)_|_ =< (a_|_ v c_|_)
7	6	lelor 158	. . . . . . 7 ((b v c_|_) v (b v c_|_)_|_) =< ((b v c_|_) v (a_|_ v c_|_))
8	1, 7	bltr 130	. . . . . 6 1 =< ((b v c_|_) v (a_|_ v c_|_))
9	8	lelan 159	. . . . 5 (a ^ 1) =< (a ^ ((b v c_|_) v (a_|_ v c_|_)))
10		an1 98	. . . . 5 (a ^ 1) = a
11		comor1 443	. . . . . . 7 (a_|_ v c_|_) C a_|_
12	11	comcom7 442	. . . . . 6 (a_|_ v c_|_) C a
13		df-a 39	. . . . . . . . . 10 (a ^ c) = (a_|_ v c_|_)_|_
14	13	ax-r1 34	. . . . . . . . 9 (a_|_ v c_|_)_|_ = (a ^ c)
15	14, 2	bltr 130	. . . . . . . 8 (a_|_ v c_|_)_|_ =< (b v c_|_)
16	15	lecom 172	. . . . . . 7 (a_|_ v c_|_)_|_ C (b v c_|_)
17	16	comcom6 441	. . . . . 6 (a_|_ v c_|_) C (b v c_|_)
18	12, 17	fh2c 459	. . . . 5 (a ^ ((b v c_|_) v (a_|_ v c_|_))) = ((a ^ (b v c_|_)) v (a ^ (a_|_ v c_|_)))
19	9, 10, 18	le3tr2 133	. . . 4 a =< ((a ^ (b v c_|_)) v (a ^ (a_|_ v c_|_)))
20		elimcons.1	. . . . . . . . 9 (a ->1 c) = (b ->1 c)
21		df-i1 43	. . . . . . . . 9 (a ->1 c) = (a_|_ v (a ^ c))
22		df-i1 43	. . . . . . . . 9 (b ->1 c) = (b_|_ v (b ^ c))
23	20, 21, 22	3tr2 61	. . . . . . . 8 (a_|_ v (a ^ c)) = (b_|_ v (b ^ c))
24	13	lor 66	. . . . . . . 8 (a_|_ v (a ^ c)) = (a_|_ v (a_|_ v c_|_)_|_)
25		df-a 39	. . . . . . . . 9 (b ^ c) = (b_|_ v c_|_)_|_
26	25	lor 66	. . . . . . . 8 (b_|_ v (b ^ c)) = (b_|_ v (b_|_ v c_|_)_|_)
27	23, 24, 26	3tr2 61	. . . . . . 7 (a_|_ v (a_|_ v c_|_)_|_) = (b_|_ v (b_|_ v c_|_)_|_)
28	27	ax-r4 36	. . . . . 6 (a_|_ v (a_|_ v c_|_)_|_)_|_ = (b_|_ v (b_|_ v c_|_)_|_)_|_
29		df-a 39	. . . . . 6 (a ^ (a_|_ v c_|_)) = (a_|_ v (a_|_ v c_|_)_|_)_|_
30		df-a 39	. . . . . 6 (b ^ (b_|_ v c_|_)) = (b_|_ v (b_|_ v c_|_)_|_)_|_
31	28, 29, 30	3tr1 60	. . . . 5 (a ^ (a_|_ v c_|_)) = (b ^ (b_|_ v c_|_))
32	31	lor 66	. . . 4 ((a ^ (b v c_|_)) v (a ^ (a_|_ v c_|_))) = ((a ^ (b v c_|_)) v (b ^ (b_|_ v c_|_)))
33	19, 32	lbtr 131	. . 3 a =< ((a ^ (b v c_|_)) v (b ^ (b_|_ v c_|_)))
34		lear 153	. . . 4 (a ^ (b v c_|_)) =< (b v c_|_)
35	34	leror 144	. . 3 ((a ^ (b v c_|_)) v (b ^ (b_|_ v c_|_))) =< ((b v c_|_) v (b ^ (b_|_ v c_|_)))
36	33, 35	letr 129	. 2 a =< ((b v c_|_) v (b ^ (b_|_ v c_|_)))
37		ax-a2 30	. . 3 ((b v c_|_) v (b ^ (b_|_ v c_|_))) = ((b ^ (b_|_ v c_|_)) v (b v c_|_))
38		leao1 154	. . . 4 (b ^ (b_|_ v c_|_)) =< (b v c_|_)
39	38	df-le2 123	. . 3 ((b ^ (b_|_ v c_|_)) v (b v c_|_)) = (b v c_|_)
40	37, 39	ax-r2 35	. 2 ((b v c_|_) v (b ^ (b_|_ v c_|_))) = (b v c_|_)
41	36, 40	lbtr 131	1 a =< (b v c_|_)

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

This theorem is referenced by:  elimcons 850

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