Theorem oa3-3lem 961

Description: Lemma for 3-OA(3). Equivalence with substitution into 6-OA dual.

Assertion

Ref	Expression
oa3-3lem	(a_|_ ^ (a v (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c))))))) = (a_|_ ^ (a v (b ^ ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))

Proof of Theorem oa3-3lem

Step	Hyp	Ref	Expression
1		dfb 86	. . . . . 6 (a == b) = ((a ^ b) v (a_|_ ^ b_|_))
2	1	ax-r1 34	. . . . 5 ((a ^ b) v (a_|_ ^ b_|_)) = (a == b)
3		an1 98	. . . . . . . . 9 (a ^ 1) = a
4		ax-a1 29	. . . . . . . . 9 a = a_|__|_
5	3, 4	ax-r2 35	. . . . . . . 8 (a ^ 1) = a_|__|_
6	5	ax-r5 37	. . . . . . 7 ((a ^ 1) v (a_|_ ^ c)) = (a_|__|_ v (a_|_ ^ c))
7		df-i1 43	. . . . . . . 8 (a_|_ ->1 c) = (a_|__|_ v (a_|_ ^ c))
8	7	ax-r1 34	. . . . . . 7 (a_|__|_ v (a_|_ ^ c)) = (a_|_ ->1 c)
9	6, 8	ax-r2 35	. . . . . 6 ((a ^ 1) v (a_|_ ^ c)) = (a_|_ ->1 c)
10		an1 98	. . . . . . . . 9 (b ^ 1) = b
11		ax-a1 29	. . . . . . . . 9 b = b_|__|_
12	10, 11	ax-r2 35	. . . . . . . 8 (b ^ 1) = b_|__|_
13	12	ax-r5 37	. . . . . . 7 ((b ^ 1) v (b_|_ ^ c)) = (b_|__|_ v (b_|_ ^ c))
14		df-i1 43	. . . . . . . 8 (b_|_ ->1 c) = (b_|__|_ v (b_|_ ^ c))
15	14	ax-r1 34	. . . . . . 7 (b_|__|_ v (b_|_ ^ c)) = (b_|_ ->1 c)
16	13, 15	ax-r2 35	. . . . . 6 ((b ^ 1) v (b_|_ ^ c)) = (b_|_ ->1 c)
17	9, 16	2an 72	. . . . 5 (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c))) = ((a_|_ ->1 c) ^ (b_|_ ->1 c))
18	2, 17	2or 67	. . . 4 (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c)))) = ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))
19	18	lan 70	. . 3 (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c))))) = (b ^ ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))
20	19	lor 66	. 2 (a v (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c)))))) = (a v (b ^ ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c)))))
21	20	lan 70	1 (a_|_ ^ (a v (b ^ (((a ^ b) v (a_|_ ^ b_|_)) v (((a ^ 1) v (a_|_ ^ c)) ^ ((b ^ 1) v (b_|_ ^ c))))))) = (a_|_ ^ (a v (b ^ ((a == b) v ((a_|_ ->1 c) ^ (b_|_ ->1 c))))))

Syntax hints:   = wb 1  _|_wn 4   == tb 5   v wo 6   ^ wa 7  1wt 9   ->1 wi1 13

This theorem is referenced by:  oa3-6to3 967

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43

metamath.org