Theorem mccune2 239

Description: E2 - OL theorem proved by EQP

Assertion

Ref	Expression
mccune2	(a v ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))))) = 1

Proof of Theorem mccune2

Step	Hyp	Ref	Expression
1		ax-a3 31	. . 3 ((a v ((a v b_|_) ^ (a v b))_|_) v (a v ((a v b_|_) ^ (a v b))_|_)_|_) = (a v (((a v b_|_) ^ (a v b))_|_ v (a v ((a v b_|_) ^ (a v b))_|_)_|_))
2	1	ax-r1 34	. 2 (a v (((a v b_|_) ^ (a v b))_|_ v (a v ((a v b_|_) ^ (a v b))_|_)_|_)) = ((a v ((a v b_|_) ^ (a v b))_|_) v (a v ((a v b_|_) ^ (a v b))_|_)_|_)
3		anor2 81	. . . . 5 (a_|_ ^ ((a v b_|_) ^ (a v b))) = (a v ((a v b_|_) ^ (a v b))_|_)_|_
4		lear 153	. . . . . . 7 (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) =< ((a_|_ ^ b) v (a_|_ ^ b_|_))
5		lea 152	. . . . . . . . 9 (a_|_ ^ b) =< a_|_
6		lea 152	. . . . . . . . 9 (a_|_ ^ b_|_) =< a_|_
7	5, 6	lel2or 162	. . . . . . . 8 ((a_|_ ^ b) v (a_|_ ^ b_|_)) =< a_|_
8		id 58	. . . . . . . . 9 ((a_|_ ^ b) v (a_|_ ^ b_|_)) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
9	8	bile 134	. . . . . . . 8 ((a_|_ ^ b) v (a_|_ ^ b_|_)) =< ((a_|_ ^ b) v (a_|_ ^ b_|_))
10	7, 9	ler2an 165	. . . . . . 7 ((a_|_ ^ b) v (a_|_ ^ b_|_)) =< (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_)))
11	4, 10	lebi 137	. . . . . 6 (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) = ((a_|_ ^ b) v (a_|_ ^ b_|_))
12		anor2 81	. . . . . . . 8 (a_|_ ^ b) = (a v b_|_)_|_
13		anor3 82	. . . . . . . 8 (a_|_ ^ b_|_) = (a v b)_|_
14	12, 13	2or 67	. . . . . . 7 ((a_|_ ^ b) v (a_|_ ^ b_|_)) = ((a v b_|_)_|_ v (a v b)_|_)
15		oran3 85	. . . . . . 7 ((a v b_|_)_|_ v (a v b)_|_) = ((a v b_|_) ^ (a v b))_|_
16	14, 15	ax-r2 35	. . . . . 6 ((a_|_ ^ b) v (a_|_ ^ b_|_)) = ((a v b_|_) ^ (a v b))_|_
17	11, 16	ax-r2 35	. . . . 5 (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))) = ((a v b_|_) ^ (a v b))_|_
18	3, 17	2or 67	. . . 4 ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_)))) = ((a v ((a v b_|_) ^ (a v b))_|_)_|_ v ((a v b_|_) ^ (a v b))_|_)
19		ax-a2 30	. . . 4 ((a v ((a v b_|_) ^ (a v b))_|_)_|_ v ((a v b_|_) ^ (a v b))_|_) = (((a v b_|_) ^ (a v b))_|_ v (a v ((a v b_|_) ^ (a v b))_|_)_|_)
20	18, 19	ax-r2 35	. . 3 ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_)))) = (((a v b_|_) ^ (a v b))_|_ v (a v ((a v b_|_) ^ (a v b))_|_)_|_)
21	20	lor 66	. 2 (a v ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))))) = (a v (((a v b_|_) ^ (a v b))_|_ v (a v ((a v b_|_) ^ (a v b))_|_)_|_))
22		df-t 40	. 2 1 = ((a v ((a v b_|_) ^ (a v b))_|_) v (a v ((a v b_|_) ^ (a v b))_|_)_|_)
23	2, 21, 22	3tr1 60	1 (a v ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a_|_ ^ b) v (a_|_ ^ b_|_))))) = 1

Syntax hints:   = wb 1  _|_wn 4   v wo 6   ^ wa 7  1wt 9

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

This theorem depends on definitions:  df-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123

metamath.org