Theorem elimcons 868

Description: Consequent elimination law. (Contributed by NM, 3-Mar-2002.)

Hypotheses

Ref	Expression
elimcons.1	(a →1 c) = (b →1 c)
elimcons.2	(a ∩ c) ≤ (b ∪ c⊥ )

Assertion

Ref	Expression
elimcons	a ≤ b

Proof of Theorem elimcons

Step	Hyp	Ref	Expression
1		df-t 41	. . . . . . . 8 1 = (a ∪ a⊥ )
2		elimcons.1	. . . . . . . . . 10 (a →1 c) = (b →1 c)
3		elimcons.2	. . . . . . . . . 10 (a ∩ c) ≤ (b ∪ c⊥ )
4	2, 3	elimconslem 867	. . . . . . . . 9 a ≤ (b ∪ c⊥ )
5	4	leror 152	. . . . . . . 8 (a ∪ a⊥ ) ≤ ((b ∪ c⊥ ) ∪ a⊥ )
6	1, 5	bltr 138	. . . . . . 7 1 ≤ ((b ∪ c⊥ ) ∪ a⊥ )
7	6	lelan 167	. . . . . 6 (b⊥ ∩ 1) ≤ (b⊥ ∩ ((b ∪ c⊥ ) ∪ a⊥ ))
8		an1 106	. . . . . 6 (b⊥ ∩ 1) = b⊥
9		comor1 461	. . . . . . . 8 (b ∪ c⊥ ) C b
10	9	comcom2 183	. . . . . . 7 (b ∪ c⊥ ) C b⊥
11	4	lecom 180	. . . . . . . . 9 a C (b ∪ c⊥ )
12	11	comcom3 454	. . . . . . . 8 a⊥ C (b ∪ c⊥ )
13	12	comcom 453	. . . . . . 7 (b ∪ c⊥ ) C a⊥
14	10, 13	fh2 470	. . . . . 6 (b⊥ ∩ ((b ∪ c⊥ ) ∪ a⊥ )) = ((b⊥ ∩ (b ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ ))
15	7, 8, 14	le3tr2 141	. . . . 5 b⊥ ≤ ((b⊥ ∩ (b ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ ))
16	2	negant 852	. . . . . . . . . . 11 (a⊥ →1 c) = (b⊥ →1 c)
17		df-i1 44	. . . . . . . . . . 11 (a⊥ →1 c) = (a⊥ ⊥ ∪ (a⊥ ∩ c))
18		df-i1 44	. . . . . . . . . . 11 (b⊥ →1 c) = (b⊥ ⊥ ∪ (b⊥ ∩ c))
19	16, 17, 18	3tr2 64	. . . . . . . . . 10 (a⊥ ⊥ ∪ (a⊥ ∩ c)) = (b⊥ ⊥ ∪ (b⊥ ∩ c))
20		anor2 89	. . . . . . . . . . 11 (a⊥ ∩ c) = (a ∪ c⊥ )⊥
21	20	lor 70	. . . . . . . . . 10 (a⊥ ⊥ ∪ (a⊥ ∩ c)) = (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ )
22		anor2 89	. . . . . . . . . . 11 (b⊥ ∩ c) = (b ∪ c⊥ )⊥
23	22	lor 70	. . . . . . . . . 10 (b⊥ ⊥ ∪ (b⊥ ∩ c)) = (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ )
24	19, 21, 23	3tr2 64	. . . . . . . . 9 (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ ) = (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ )
25	24	ax-r1 35	. . . . . . . 8 (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ ) = (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ )
26	25	ax-r4 37	. . . . . . 7 (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ )⊥ = (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ )⊥
27		df-a 40	. . . . . . 7 (b⊥ ∩ (b ∪ c⊥ )) = (b⊥ ⊥ ∪ (b ∪ c⊥ )⊥ )⊥
28		df-a 40	. . . . . . 7 (a⊥ ∩ (a ∪ c⊥ )) = (a⊥ ⊥ ∪ (a ∪ c⊥ )⊥ )⊥
29	26, 27, 28	3tr1 63	. . . . . 6 (b⊥ ∩ (b ∪ c⊥ )) = (a⊥ ∩ (a ∪ c⊥ ))
30	29	ax-r5 38	. . . . 5 ((b⊥ ∩ (b ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ )) = ((a⊥ ∩ (a ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ ))
31	15, 30	lbtr 139	. . . 4 b⊥ ≤ ((a⊥ ∩ (a ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ ))
32		lear 161	. . . . 5 (b⊥ ∩ a⊥ ) ≤ a⊥
33	32	lelor 166	. . . 4 ((a⊥ ∩ (a ∪ c⊥ )) ∪ (b⊥ ∩ a⊥ )) ≤ ((a⊥ ∩ (a ∪ c⊥ )) ∪ a⊥ )
34	31, 33	letr 137	. . 3 b⊥ ≤ ((a⊥ ∩ (a ∪ c⊥ )) ∪ a⊥ )
35		lea 160	. . . 4 (a⊥ ∩ (a ∪ c⊥ )) ≤ a⊥
36	35	df-le2 131	. . 3 ((a⊥ ∩ (a ∪ c⊥ )) ∪ a⊥ ) = a⊥
37	34, 36	lbtr 139	. 2 b⊥ ≤ a⊥
38	37	lecon1 155	1 a ≤ b

Syntax hints:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-i1 44  df-le1 130  df-le2 131  df-c1 132  df-c2 133

This theorem is referenced by:  elimcons2  869