Theorem comanblem2 853

Description: Lemma for biconditional commutation law.

Assertion

Ref	Expression
comanblem2	((a ^ b) ^ ((a == c) ^ (b == c))) = ((a ^ b) ^ c)

Proof of Theorem comanblem2

Step	Hyp	Ref	Expression
1		dfb 86	. . . 4 (a == c) = ((a ^ c) v (a_|_ ^ c_|_))
2		dfb 86	. . . 4 (b == c) = ((b ^ c) v (b_|_ ^ c_|_))
3	1, 2	2an 72	. . 3 ((a == c) ^ (b == c)) = (((a ^ c) v (a_|_ ^ c_|_)) ^ ((b ^ c) v (b_|_ ^ c_|_)))
4	3	lan 70	. 2 ((a ^ b) ^ ((a == c) ^ (b == c))) = ((a ^ b) ^ (((a ^ c) v (a_|_ ^ c_|_)) ^ ((b ^ c) v (b_|_ ^ c_|_))))
5		comanr1 446	. . . . . 6 a C (a ^ c)
6		comanr1 446	. . . . . . 7 a_|_ C (a_|_ ^ c_|_)
7	6	comcom6 441	. . . . . 6 a C (a_|_ ^ c_|_)
8	5, 7	fh1 451	. . . . 5 (a ^ ((a ^ c) v (a_|_ ^ c_|_))) = ((a ^ (a ^ c)) v (a ^ (a_|_ ^ c_|_)))
9		anass 69	. . . . . . . 8 ((a ^ a) ^ c) = (a ^ (a ^ c))
10	9	ax-r1 34	. . . . . . 7 (a ^ (a ^ c)) = ((a ^ a) ^ c)
11		anidm 103	. . . . . . . 8 (a ^ a) = a
12	11	ran 71	. . . . . . 7 ((a ^ a) ^ c) = (a ^ c)
13	10, 12	ax-r2 35	. . . . . 6 (a ^ (a ^ c)) = (a ^ c)
14		dff 93	. . . . . . . . 9 0 = (a ^ a_|_)
15	14	ran 71	. . . . . . . 8 (0 ^ c_|_) = ((a ^ a_|_) ^ c_|_)
16	15	ax-r1 34	. . . . . . 7 ((a ^ a_|_) ^ c_|_) = (0 ^ c_|_)
17		anass 69	. . . . . . 7 ((a ^ a_|_) ^ c_|_) = (a ^ (a_|_ ^ c_|_))
18		an0r 101	. . . . . . 7 (0 ^ c_|_) = 0
19	16, 17, 18	3tr2 61	. . . . . 6 (a ^ (a_|_ ^ c_|_)) = 0
20	13, 19	2or 67	. . . . 5 ((a ^ (a ^ c)) v (a ^ (a_|_ ^ c_|_))) = ((a ^ c) v 0)
21		or0 94	. . . . 5 ((a ^ c) v 0) = (a ^ c)
22	8, 20, 21	3tr 62	. . . 4 (a ^ ((a ^ c) v (a_|_ ^ c_|_))) = (a ^ c)
23		comanr1 446	. . . . . 6 b C (b ^ c)
24		comanr1 446	. . . . . . 7 b_|_ C (b_|_ ^ c_|_)
25	24	comcom6 441	. . . . . 6 b C (b_|_ ^ c_|_)
26	23, 25	fh1 451	. . . . 5 (b ^ ((b ^ c) v (b_|_ ^ c_|_))) = ((b ^ (b ^ c)) v (b ^ (b_|_ ^ c_|_)))
27		anass 69	. . . . . . . 8 ((b ^ b) ^ c) = (b ^ (b ^ c))
28	27	ax-r1 34	. . . . . . 7 (b ^ (b ^ c)) = ((b ^ b) ^ c)
29		anidm 103	. . . . . . . 8 (b ^ b) = b
30	29	ran 71	. . . . . . 7 ((b ^ b) ^ c) = (b ^ c)
31	28, 30	ax-r2 35	. . . . . 6 (b ^ (b ^ c)) = (b ^ c)
32		dff 93	. . . . . . . . 9 0 = (b ^ b_|_)
33	32	ran 71	. . . . . . . 8 (0 ^ c_|_) = ((b ^ b_|_) ^ c_|_)
34	33	ax-r1 34	. . . . . . 7 ((b ^ b_|_) ^ c_|_) = (0 ^ c_|_)
35		anass 69	. . . . . . 7 ((b ^ b_|_) ^ c_|_) = (b ^ (b_|_ ^ c_|_))
36	34, 35, 18	3tr2 61	. . . . . 6 (b ^ (b_|_ ^ c_|_)) = 0
37	31, 36	2or 67	. . . . 5 ((b ^ (b ^ c)) v (b ^ (b_|_ ^ c_|_))) = ((b ^ c) v 0)
38		or0 94	. . . . 5 ((b ^ c) v 0) = (b ^ c)
39	26, 37, 38	3tr 62	. . . 4 (b ^ ((b ^ c) v (b_|_ ^ c_|_))) = (b ^ c)
40	22, 39	2an 72	. . 3 ((a ^ ((a ^ c) v (a_|_ ^ c_|_))) ^ (b ^ ((b ^ c) v (b_|_ ^ c_|_)))) = ((a ^ c) ^ (b ^ c))
41		an4 78	. . 3 ((a ^ b) ^ (((a ^ c) v (a_|_ ^ c_|_)) ^ ((b ^ c) v (b_|_ ^ c_|_)))) = ((a ^ ((a ^ c) v (a_|_ ^ c_|_))) ^ (b ^ ((b ^ c) v (b_|_ ^ c_|_))))
42		anandir 107	. . 3 ((a ^ b) ^ c) = ((a ^ c) ^ (b ^ c))
43	40, 41, 42	3tr1 60	. 2 ((a ^ b) ^ (((a ^ c) v (a_|_ ^ c_|_)) ^ ((b ^ c) v (b_|_ ^ c_|_)))) = ((a ^ b) ^ c)
44	4, 43	ax-r2 35	1 ((a ^ b) ^ ((a == c) ^ (b == c))) = ((a ^ b) ^ c)

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v wo 6   ^ wa 7  0wf 10

This theorem is referenced by:  comanb 854

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

metamath.org