Theorem u24lem 752

Description: Lemma for unified implication study.

Assertion

Ref	Expression
u24lem	((a ->2 b) ^ (a ->4 b)) = (a ->5 b)

Proof of Theorem u24lem

Step	Hyp	Ref	Expression
1		df-i2 44	. . 3 (a ->2 b) = (b v (a_|_ ^ b_|_))
2	1	ran 71	. 2 ((a ->2 b) ^ (a ->4 b)) = ((b v (a_|_ ^ b_|_)) ^ (a ->4 b))
3		u4lemc1 665	. . . 4 b C (a ->4 b)
4		comanr2 447	. . . . 5 b_|_ C (a_|_ ^ b_|_)
5	4	comcom6 441	. . . 4 b C (a_|_ ^ b_|_)
6	3, 5	fh2r 456	. . 3 ((b v (a_|_ ^ b_|_)) ^ (a ->4 b)) = ((b ^ (a ->4 b)) v ((a_|_ ^ b_|_) ^ (a ->4 b)))
7		ancom 68	. . . . . 6 (b ^ (a ->4 b)) = ((a ->4 b) ^ b)
8		ancom 68	. . . . . 6 ((a ->4 b) ^ b) = (b ^ (a ->4 b))
9	7, 8	ax-r2 35	. . . . 5 (b ^ (a ->4 b)) = (b ^ (a ->4 b))
10		anass 69	. . . . . 6 ((a_|_ ^ b_|_) ^ (a ->4 b)) = (a_|_ ^ (b_|_ ^ (a ->4 b)))
11		ancom 68	. . . . . . . . 9 (b_|_ ^ (a ->4 b)) = ((a ->4 b) ^ b_|_)
12		u4lemanb 600	. . . . . . . . 9 ((a ->4 b) ^ b_|_) = ((a_|_ v b) ^ b_|_)
13	11, 12	ax-r2 35	. . . . . . . 8 (b_|_ ^ (a ->4 b)) = ((a_|_ v b) ^ b_|_)
14	13	lan 70	. . . . . . 7 (a_|_ ^ (b_|_ ^ (a ->4 b))) = (a_|_ ^ ((a_|_ v b) ^ b_|_))
15		anass 69	. . . . . . . . 9 ((a_|_ ^ (a_|_ v b)) ^ b_|_) = (a_|_ ^ ((a_|_ v b) ^ b_|_))
16	15	ax-r1 34	. . . . . . . 8 (a_|_ ^ ((a_|_ v b) ^ b_|_)) = ((a_|_ ^ (a_|_ v b)) ^ b_|_)
17		a5c 113	. . . . . . . . . 10 (a_|_ ^ (a_|_ v b)) = a_|_
18	17	ran 71	. . . . . . . . 9 ((a_|_ ^ (a_|_ v b)) ^ b_|_) = (a_|_ ^ b_|_)
19		ancom 68	. . . . . . . . 9 (a_|_ ^ b_|_) = (b_|_ ^ a_|_)
20	18, 19	ax-r2 35	. . . . . . . 8 ((a_|_ ^ (a_|_ v b)) ^ b_|_) = (b_|_ ^ a_|_)
21	16, 20	ax-r2 35	. . . . . . 7 (a_|_ ^ ((a_|_ v b) ^ b_|_)) = (b_|_ ^ a_|_)
22	14, 21	ax-r2 35	. . . . . 6 (a_|_ ^ (b_|_ ^ (a ->4 b))) = (b_|_ ^ a_|_)
23	10, 22	ax-r2 35	. . . . 5 ((a_|_ ^ b_|_) ^ (a ->4 b)) = (b_|_ ^ a_|_)
24	9, 23	2or 67	. . . 4 ((b ^ (a ->4 b)) v ((a_|_ ^ b_|_) ^ (a ->4 b))) = ((b ^ (a ->4 b)) v (b_|_ ^ a_|_))
25		comanr1 446	. . . . . . 7 b_|_ C (b_|_ ^ a_|_)
26	25	comcom6 441	. . . . . 6 b C (b_|_ ^ a_|_)
27	26, 3	fh4r 458	. . . . 5 ((b ^ (a ->4 b)) v (b_|_ ^ a_|_)) = ((b v (b_|_ ^ a_|_)) ^ ((a ->4 b) v (b_|_ ^ a_|_)))
28	3, 26	com2or 465	. . . . . . 7 b C ((a ->4 b) v (b_|_ ^ a_|_))
29	28, 26	fh2r 456	. . . . . 6 ((b v (b_|_ ^ a_|_)) ^ ((a ->4 b) v (b_|_ ^ a_|_))) = ((b ^ ((a ->4 b) v (b_|_ ^ a_|_))) v ((b_|_ ^ a_|_) ^ ((a ->4 b) v (b_|_ ^ a_|_))))
30	3, 26	fh1 451	. . . . . . . . 9 (b ^ ((a ->4 b) v (b_|_ ^ a_|_))) = ((b ^ (a ->4 b)) v (b ^ (b_|_ ^ a_|_)))
31		u4lemab 595	. . . . . . . . . . . 12 ((a ->4 b) ^ b) = ((a ^ b) v (a_|_ ^ b))
32	7, 31	ax-r2 35	. . . . . . . . . . 11 (b ^ (a ->4 b)) = ((a ^ b) v (a_|_ ^ b))
33	32	ax-r5 37	. . . . . . . . . 10 ((b ^ (a ->4 b)) v (b ^ (b_|_ ^ a_|_))) = (((a ^ b) v (a_|_ ^ b)) v (b ^ (b_|_ ^ a_|_)))
34		id 58	. . . . . . . . . 10 (((a ^ b) v (a_|_ ^ b)) v (b ^ (b_|_ ^ a_|_))) = (((a ^ b) v (a_|_ ^ b)) v (b ^ (b_|_ ^ a_|_)))
35	33, 34	ax-r2 35	. . . . . . . . 9 ((b ^ (a ->4 b)) v (b ^ (b_|_ ^ a_|_))) = (((a ^ b) v (a_|_ ^ b)) v (b ^ (b_|_ ^ a_|_)))
36	30, 35	ax-r2 35	. . . . . . . 8 (b ^ ((a ->4 b) v (b_|_ ^ a_|_))) = (((a ^ b) v (a_|_ ^ b)) v (b ^ (b_|_ ^ a_|_)))
37		leor 151	. . . . . . . . 9 (b_|_ ^ a_|_) =< ((a ->4 b) v (b_|_ ^ a_|_))
38	37	df2le2 128	. . . . . . . 8 ((b_|_ ^ a_|_) ^ ((a ->4 b) v (b_|_ ^ a_|_))) = (b_|_ ^ a_|_)
39	36, 38	2or 67	. . . . . . 7 ((b ^ ((a ->4 b) v (b_|_ ^ a_|_))) v ((b_|_ ^ a_|_) ^ ((a ->4 b) v (b_|_ ^ a_|_)))) = ((((a ^ b) v (a_|_ ^ b)) v (b ^ (b_|_ ^ a_|_))) v (b_|_ ^ a_|_))
40		ax-a3 31	. . . . . . . 8 ((((a ^ b) v (a_|_ ^ b)) v (b ^ (b_|_ ^ a_|_))) v (b_|_ ^ a_|_)) = (((a ^ b) v (a_|_ ^ b)) v ((b ^ (b_|_ ^ a_|_)) v (b_|_ ^ a_|_)))
41		lear 153	. . . . . . . . . . . 12 (b ^ (b_|_ ^ a_|_)) =< (b_|_ ^ a_|_)
42	41	df-le2 123	. . . . . . . . . . 11 ((b ^ (b_|_ ^ a_|_)) v (b_|_ ^ a_|_)) = (b_|_ ^ a_|_)
43		ancom 68	. . . . . . . . . . 11 (b_|_ ^ a_|_) = (a_|_ ^ b_|_)
44	42, 43	ax-r2 35	. . . . . . . . . 10 ((b ^ (b_|_ ^ a_|_)) v (b_|_ ^ a_|_)) = (a_|_ ^ b_|_)
45	44	lor 66	. . . . . . . . 9 (((a ^ b) v (a_|_ ^ b)) v ((b ^ (b_|_ ^ a_|_)) v (b_|_ ^ a_|_))) = (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_))
46		df-i5 47	. . . . . . . . . . 11 (a ->5 b) = (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_))
47	46	ax-r1 34	. . . . . . . . . 10 (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) = (a ->5 b)
48		id 58	. . . . . . . . . 10 (a ->5 b) = (a ->5 b)
49	47, 48	ax-r2 35	. . . . . . . . 9 (((a ^ b) v (a_|_ ^ b)) v (a_|_ ^ b_|_)) = (a ->5 b)
50	45, 49	ax-r2 35	. . . . . . . 8 (((a ^ b) v (a_|_ ^ b)) v ((b ^ (b_|_ ^ a_|_)) v (b_|_ ^ a_|_))) = (a ->5 b)
51	40, 50	ax-r2 35	. . . . . . 7 ((((a ^ b) v (a_|_ ^ b)) v (b ^ (b_|_ ^ a_|_))) v (b_|_ ^ a_|_)) = (a ->5 b)
52	39, 51	ax-r2 35	. . . . . 6 ((b ^ ((a ->4 b) v (b_|_ ^ a_|_))) v ((b_|_ ^ a_|_) ^ ((a ->4 b) v (b_|_ ^ a_|_)))) = (a ->5 b)
53	29, 52	ax-r2 35	. . . . 5 ((b v (b_|_ ^ a_|_)) ^ ((a ->4 b) v (b_|_ ^ a_|_))) = (a ->5 b)
54	27, 53	ax-r2 35	. . . 4 ((b ^ (a ->4 b)) v (b_|_ ^ a_|_)) = (a ->5 b)
55	24, 54	ax-r2 35	. . 3 ((b ^ (a ->4 b)) v ((a_|_ ^ b_|_) ^ (a ->4 b))) = (a ->5 b)
56	6, 55	ax-r2 35	. 2 ((b v (a_|_ ^ b_|_)) ^ (a ->4 b)) = (a ->5 b)
57	2, 56	ax-r2 35	1 ((a ->2 b) ^ (a ->4 b)) = (a ->5 b)

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7   ->2 wi2 14   ->4 wi4 16   ->5 wi5 17

This theorem is referenced by:  negant5 845

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-i2 44  df-i4 46  df-i5 47  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org