Theorem cancellem 873

Description: Lemma for cancellation law eliminating ->1 consequent.

Hypothesis

Ref	Expression
cancel.1	((d v (a ->1 c)) ->1 c) = ((d v (b ->1 c)) ->1 c)

Assertion

Ref	Expression
cancellem	(d v (a ->1 c)) =< (d v (b ->1 c))

Proof of Theorem cancellem

Step	Hyp	Ref	Expression
1		i1abs 783	. . 3 (((d v (a ->1 c)) ->1 c)_|_ v ((d v (a ->1 c)) ^ c)) = (d v (a ->1 c))
2	1	ax-r1 34	. 2 (d v (a ->1 c)) = (((d v (a ->1 c)) ->1 c)_|_ v ((d v (a ->1 c)) ^ c))
3		leo 150	. . . . 5 (d v (b ->1 c))_|_ =< ((d v (b ->1 c))_|_ v ((d v (b ->1 c)) ^ c))
4		cancel.1	. . . . . . 7 ((d v (a ->1 c)) ->1 c) = ((d v (b ->1 c)) ->1 c)
5		df-i1 43	. . . . . . 7 ((d v (b ->1 c)) ->1 c) = ((d v (b ->1 c))_|_ v ((d v (b ->1 c)) ^ c))
6	4, 5	ax-r2 35	. . . . . 6 ((d v (a ->1 c)) ->1 c) = ((d v (b ->1 c))_|_ v ((d v (b ->1 c)) ^ c))
7	6	ax-r1 34	. . . . 5 ((d v (b ->1 c))_|_ v ((d v (b ->1 c)) ^ c)) = ((d v (a ->1 c)) ->1 c)
8	3, 7	lbtr 131	. . . 4 (d v (b ->1 c))_|_ =< ((d v (a ->1 c)) ->1 c)
9	8	lecon2 148	. . 3 ((d v (a ->1 c)) ->1 c)_|_ =< (d v (b ->1 c))
10		leor 151	. . . . . 6 ((d v (a ->1 c)) ^ c) =< ((d v (a ->1 c))_|_ v ((d v (a ->1 c)) ^ c))
11		df-i1 43	. . . . . . . 8 ((d v (a ->1 c)) ->1 c) = ((d v (a ->1 c))_|_ v ((d v (a ->1 c)) ^ c))
12	11	ax-r1 34	. . . . . . 7 ((d v (a ->1 c))_|_ v ((d v (a ->1 c)) ^ c)) = ((d v (a ->1 c)) ->1 c)
13	12, 4	ax-r2 35	. . . . . 6 ((d v (a ->1 c))_|_ v ((d v (a ->1 c)) ^ c)) = ((d v (b ->1 c)) ->1 c)
14	10, 13	lbtr 131	. . . . 5 ((d v (a ->1 c)) ^ c) =< ((d v (b ->1 c)) ->1 c)
15		lear 153	. . . . 5 ((d v (a ->1 c)) ^ c) =< c
16	14, 15	ler2an 165	. . . 4 ((d v (a ->1 c)) ^ c) =< (((d v (b ->1 c)) ->1 c) ^ c)
17		coman2 178	. . . . . . 7 ((d v (b ->1 c)) ^ c) C c
18		coman1 177	. . . . . . . 8 ((d v (b ->1 c)) ^ c) C (d v (b ->1 c))
19	18	comcom2 175	. . . . . . 7 ((d v (b ->1 c)) ^ c) C (d v (b ->1 c))_|_
20	17, 19	fh2rc 462	. . . . . 6 (((d v (b ->1 c))_|_ v ((d v (b ->1 c)) ^ c)) ^ c) = (((d v (b ->1 c))_|_ ^ c) v (((d v (b ->1 c)) ^ c) ^ c))
21	5	ran 71	. . . . . 6 (((d v (b ->1 c)) ->1 c) ^ c) = (((d v (b ->1 c))_|_ v ((d v (b ->1 c)) ^ c)) ^ c)
22		id 58	. . . . . 6 (((d v (b ->1 c))_|_ ^ c) v (((d v (b ->1 c)) ^ c) ^ c)) = (((d v (b ->1 c))_|_ ^ c) v (((d v (b ->1 c)) ^ c) ^ c))
23	20, 21, 22	3tr1 60	. . . . 5 (((d v (b ->1 c)) ->1 c) ^ c) = (((d v (b ->1 c))_|_ ^ c) v (((d v (b ->1 c)) ^ c) ^ c))
24		leao4 157	. . . . . . . 8 ((d_|_ ^ (b ^ c)_|_) ^ (b ^ c)) =< (b_|_ v (b ^ c))
25	24	lerr 142	. . . . . . 7 ((d_|_ ^ (b ^ c)_|_) ^ (b ^ c)) =< (d v (b_|_ v (b ^ c)))
26		df-i1 43	. . . . . . . . . . . 12 (b ->1 c) = (b_|_ v (b ^ c))
27	26	lor 66	. . . . . . . . . . 11 (d v (b ->1 c)) = (d v (b_|_ v (b ^ c)))
28	27	ax-r4 36	. . . . . . . . . 10 (d v (b ->1 c))_|_ = (d v (b_|_ v (b ^ c)))_|_
29		an12 74	. . . . . . . . . . . 12 (b ^ (d_|_ ^ (b ^ c)_|_)) = (d_|_ ^ (b ^ (b ^ c)_|_))
30		anor1 80	. . . . . . . . . . . . 13 (b ^ (b ^ c)_|_) = (b_|_ v (b ^ c))_|_
31	30	lan 70	. . . . . . . . . . . 12 (d_|_ ^ (b ^ (b ^ c)_|_)) = (d_|_ ^ (b_|_ v (b ^ c))_|_)
32		anor3 82	. . . . . . . . . . . 12 (d_|_ ^ (b_|_ v (b ^ c))_|_) = (d v (b_|_ v (b ^ c)))_|_
33	29, 31, 32	3tr 62	. . . . . . . . . . 11 (b ^ (d_|_ ^ (b ^ c)_|_)) = (d v (b_|_ v (b ^ c)))_|_
34	33	ax-r1 34	. . . . . . . . . 10 (d v (b_|_ v (b ^ c)))_|_ = (b ^ (d_|_ ^ (b ^ c)_|_))
35		ancom 68	. . . . . . . . . 10 (b ^ (d_|_ ^ (b ^ c)_|_)) = ((d_|_ ^ (b ^ c)_|_) ^ b)
36	28, 34, 35	3tr 62	. . . . . . . . 9 (d v (b ->1 c))_|_ = ((d_|_ ^ (b ^ c)_|_) ^ b)
37	36	ran 71	. . . . . . . 8 ((d v (b ->1 c))_|_ ^ c) = (((d_|_ ^ (b ^ c)_|_) ^ b) ^ c)
38		anass 69	. . . . . . . 8 (((d_|_ ^ (b ^ c)_|_) ^ b) ^ c) = ((d_|_ ^ (b ^ c)_|_) ^ (b ^ c))
39	37, 38	ax-r2 35	. . . . . . 7 ((d v (b ->1 c))_|_ ^ c) = ((d_|_ ^ (b ^ c)_|_) ^ (b ^ c))
40	25, 39, 27	le3tr1 132	. . . . . 6 ((d v (b ->1 c))_|_ ^ c) =< (d v (b ->1 c))
41		lea 152	. . . . . . 7 ((d v (b ->1 c)) ^ c) =< (d v (b ->1 c))
42	41	lel 143	. . . . . 6 (((d v (b ->1 c)) ^ c) ^ c) =< (d v (b ->1 c))
43	40, 42	lel2or 162	. . . . 5 (((d v (b ->1 c))_|_ ^ c) v (((d v (b ->1 c)) ^ c) ^ c)) =< (d v (b ->1 c))
44	23, 43	bltr 130	. . . 4 (((d v (b ->1 c)) ->1 c) ^ c) =< (d v (b ->1 c))
45	16, 44	letr 129	. . 3 ((d v (a ->1 c)) ^ c) =< (d v (b ->1 c))
46	9, 45	lel2or 162	. 2 (((d v (a ->1 c)) ->1 c)_|_ v ((d v (a ->1 c)) ^ c)) =< (d v (b ->1 c))
47	2, 46	bltr 130	1 (d v (a ->1 c)) =< (d v (b ->1 c))

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

This theorem is referenced by:  cancel 874

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