Theorem elimconslem 867

Description: Lemma for 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
elimconslem	a ≤ (b ∪ c⊥ )

Proof of Theorem elimconslem

Step	Hyp	Ref	Expression
1		df-t 41	. . . . . . 7 1 = ((b ∪ c⊥ ) ∪ (b ∪ c⊥ )⊥ )
2		elimcons.2	. . . . . . . . . 10 (a ∩ c) ≤ (b ∪ c⊥ )
3	2	lecon 154	. . . . . . . . 9 (b ∪ c⊥ )⊥ ≤ (a ∩ c)⊥
4		oran3 93	. . . . . . . . . 10 (a⊥ ∪ c⊥ ) = (a ∩ c)⊥
5	4	ax-r1 35	. . . . . . . . 9 (a ∩ c)⊥ = (a⊥ ∪ c⊥ )
6	3, 5	lbtr 139	. . . . . . . 8 (b ∪ c⊥ )⊥ ≤ (a⊥ ∪ c⊥ )
7	6	lelor 166	. . . . . . 7 ((b ∪ c⊥ ) ∪ (b ∪ c⊥ )⊥ ) ≤ ((b ∪ c⊥ ) ∪ (a⊥ ∪ c⊥ ))
8	1, 7	bltr 138	. . . . . 6 1 ≤ ((b ∪ c⊥ ) ∪ (a⊥ ∪ c⊥ ))
9	8	lelan 167	. . . . 5 (a ∩ 1) ≤ (a ∩ ((b ∪ c⊥ ) ∪ (a⊥ ∪ c⊥ )))
10		an1 106	. . . . 5 (a ∩ 1) = a
11		comor1 461	. . . . . . 7 (a⊥ ∪ c⊥ ) C a⊥
12	11	comcom7 460	. . . . . 6 (a⊥ ∪ c⊥ ) C a
13		df-a 40	. . . . . . . . . 10 (a ∩ c) = (a⊥ ∪ c⊥ )⊥
14	13	ax-r1 35	. . . . . . . . 9 (a⊥ ∪ c⊥ )⊥ = (a ∩ c)
15	14, 2	bltr 138	. . . . . . . 8 (a⊥ ∪ c⊥ )⊥ ≤ (b ∪ c⊥ )
16	15	lecom 180	. . . . . . 7 (a⊥ ∪ c⊥ )⊥ C (b ∪ c⊥ )
17	16	comcom6 459	. . . . . 6 (a⊥ ∪ c⊥ ) C (b ∪ c⊥ )
18	12, 17	fh2c 477	. . . . 5 (a ∩ ((b ∪ c⊥ ) ∪ (a⊥ ∪ c⊥ ))) = ((a ∩ (b ∪ c⊥ )) ∪ (a ∩ (a⊥ ∪ c⊥ )))
19	9, 10, 18	le3tr2 141	. . . 4 a ≤ ((a ∩ (b ∪ c⊥ )) ∪ (a ∩ (a⊥ ∪ c⊥ )))
20		elimcons.1	. . . . . . . . 9 (a →1 c) = (b →1 c)
21		df-i1 44	. . . . . . . . 9 (a →1 c) = (a⊥ ∪ (a ∩ c))
22		df-i1 44	. . . . . . . . 9 (b →1 c) = (b⊥ ∪ (b ∩ c))
23	20, 21, 22	3tr2 64	. . . . . . . 8 (a⊥ ∪ (a ∩ c)) = (b⊥ ∪ (b ∩ c))
24	13	lor 70	. . . . . . . 8 (a⊥ ∪ (a ∩ c)) = (a⊥ ∪ (a⊥ ∪ c⊥ )⊥ )
25		df-a 40	. . . . . . . . 9 (b ∩ c) = (b⊥ ∪ c⊥ )⊥
26	25	lor 70	. . . . . . . 8 (b⊥ ∪ (b ∩ c)) = (b⊥ ∪ (b⊥ ∪ c⊥ )⊥ )
27	23, 24, 26	3tr2 64	. . . . . . 7 (a⊥ ∪ (a⊥ ∪ c⊥ )⊥ ) = (b⊥ ∪ (b⊥ ∪ c⊥ )⊥ )
28	27	ax-r4 37	. . . . . 6 (a⊥ ∪ (a⊥ ∪ c⊥ )⊥ )⊥ = (b⊥ ∪ (b⊥ ∪ c⊥ )⊥ )⊥
29		df-a 40	. . . . . 6 (a ∩ (a⊥ ∪ c⊥ )) = (a⊥ ∪ (a⊥ ∪ c⊥ )⊥ )⊥
30		df-a 40	. . . . . 6 (b ∩ (b⊥ ∪ c⊥ )) = (b⊥ ∪ (b⊥ ∪ c⊥ )⊥ )⊥
31	28, 29, 30	3tr1 63	. . . . 5 (a ∩ (a⊥ ∪ c⊥ )) = (b ∩ (b⊥ ∪ c⊥ ))
32	31	lor 70	. . . 4 ((a ∩ (b ∪ c⊥ )) ∪ (a ∩ (a⊥ ∪ c⊥ ))) = ((a ∩ (b ∪ c⊥ )) ∪ (b ∩ (b⊥ ∪ c⊥ )))
33	19, 32	lbtr 139	. . 3 a ≤ ((a ∩ (b ∪ c⊥ )) ∪ (b ∩ (b⊥ ∪ c⊥ )))
34		lear 161	. . . 4 (a ∩ (b ∪ c⊥ )) ≤ (b ∪ c⊥ )
35	34	leror 152	. . 3 ((a ∩ (b ∪ c⊥ )) ∪ (b ∩ (b⊥ ∪ c⊥ ))) ≤ ((b ∪ c⊥ ) ∪ (b ∩ (b⊥ ∪ c⊥ )))
36	33, 35	letr 137	. 2 a ≤ ((b ∪ c⊥ ) ∪ (b ∩ (b⊥ ∪ c⊥ )))
37		ax-a2 31	. . 3 ((b ∪ c⊥ ) ∪ (b ∩ (b⊥ ∪ c⊥ ))) = ((b ∩ (b⊥ ∪ c⊥ )) ∪ (b ∪ c⊥ ))
38		leao1 162	. . . 4 (b ∩ (b⊥ ∪ c⊥ )) ≤ (b ∪ c⊥ )
39	38	df-le2 131	. . 3 ((b ∩ (b⊥ ∪ c⊥ )) ∪ (b ∪ c⊥ )) = (b ∪ c⊥ )
40	37, 39	ax-r2 36	. 2 ((b ∪ c⊥ ) ∪ (b ∩ (b⊥ ∪ c⊥ ))) = (b ∪ c⊥ )
41	36, 40	lbtr 139	1 a ≤ (b ∪ c⊥ )

This proof depends on syntax axioms:   = wb 1   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7  1wt 8   →₁ wi1 12

This proof depends on 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 proof 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 used by:  elimcons  868