Theorem u3lemana 589

Description: Lemma for Kalmbach implication study.

Assertion

Ref	Expression
u3lemana	((a ->3 b) ^ a_|_) = ((a_|_ ^ b) v (a_|_ ^ b_|_))

Proof of Theorem u3lemana

Step	Hyp	Ref	Expression
1		df-i3 45	. . 3 (a ->3 b) = (((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b)))
2	1	ran 71	. 2 ((a ->3 b) ^ a_|_) = ((((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))) ^ a_|_)
3		comanr1 446	. . . . 5 a_|_ C (a_|_ ^ b)
4		comanr1 446	. . . . 5 a_|_ C (a_|_ ^ b_|_)
5	3, 4	com2or 465	. . . 4 a_|_ C ((a_|_ ^ b) v (a_|_ ^ b_|_))
6		comid 179	. . . . . 6 a C a
7	6	comcom3 436	. . . . 5 a_|_ C a
8		comorr 176	. . . . 5 a_|_ C (a_|_ v b)
9	7, 8	com2an 466	. . . 4 a_|_ C (a ^ (a_|_ v b))
10	5, 9	fh1r 455	. . 3 ((((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))) ^ a_|_) = ((((a_|_ ^ b) v (a_|_ ^ b_|_)) ^ a_|_) v ((a ^ (a_|_ v b)) ^ a_|_))
11		lea 152	. . . . . . 7 (a_|_ ^ b) =< a_|_
12		lea 152	. . . . . . 7 (a_|_ ^ b_|_) =< a_|_
13	11, 12	lel2or 162	. . . . . 6 ((a_|_ ^ b) v (a_|_ ^ b_|_)) =< a_|_
14	13	df2le2 128	. . . . 5 (((a_|_ ^ b) v (a_|_ ^ b_|_)) ^ a_|_) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
15		an32 76	. . . . . 6 ((a ^ (a_|_ v b)) ^ a_|_) = ((a ^ a_|_) ^ (a_|_ v b))
16		ancom 68	. . . . . . 7 ((a ^ a_|_) ^ (a_|_ v b)) = ((a_|_ v b) ^ (a ^ a_|_))
17		dff 93	. . . . . . . . . 10 0 = (a ^ a_|_)
18	17	ax-r1 34	. . . . . . . . 9 (a ^ a_|_) = 0
19	18	lan 70	. . . . . . . 8 ((a_|_ v b) ^ (a ^ a_|_)) = ((a_|_ v b) ^ 0)
20		an0 100	. . . . . . . 8 ((a_|_ v b) ^ 0) = 0
21	19, 20	ax-r2 35	. . . . . . 7 ((a_|_ v b) ^ (a ^ a_|_)) = 0
22	16, 21	ax-r2 35	. . . . . 6 ((a ^ a_|_) ^ (a_|_ v b)) = 0
23	15, 22	ax-r2 35	. . . . 5 ((a ^ (a_|_ v b)) ^ a_|_) = 0
24	14, 23	2or 67	. . . 4 ((((a_|_ ^ b) v (a_|_ ^ b_|_)) ^ a_|_) v ((a ^ (a_|_ v b)) ^ a_|_)) = (((a_|_ ^ b) v (a_|_ ^ b_|_)) v 0)
25		or0 94	. . . 4 (((a_|_ ^ b) v (a_|_ ^ b_|_)) v 0) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
26	24, 25	ax-r2 35	. . 3 ((((a_|_ ^ b) v (a_|_ ^ b_|_)) ^ a_|_) v ((a ^ (a_|_ v b)) ^ a_|_)) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
27	10, 26	ax-r2 35	. 2 ((((a_|_ ^ b) v (a_|_ ^ b_|_)) v (a ^ (a_|_ v b))) ^ a_|_) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
28	2, 27	ax-r2 35	1 ((a ->3 b) ^ a_|_) = ((a_|_ ^ b) v (a_|_ ^ b_|_))

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7  0wf 10   ->3 wi3 15

This theorem is referenced by:  u3lemnoa 644  u3lem13a 771  u3lem13b 772

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-i3 45  df-le1 122  df-le2 123  df-c1 124  df-c2 125

metamath.org