Theorem wlem14 412

Description: Lemma for KA14 soundness.

Assertion

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

Proof of Theorem wlem14

Step	Hyp	Ref	Expression
1		df-t 40	. . . 4 1 = (((a ^ b_|_) v a_|_) v ((a ^ b_|_) v a_|_)_|_)
2	1	ax-r1 34	. . 3 (((a ^ b_|_) v a_|_) v ((a ^ b_|_) v a_|_)_|_) = 1
3		ax-a2 30	. . . 4 (((a ^ b_|_) v a_|_)_|_ v ((a ^ b_|_) v a_|_)) = (((a ^ b_|_) v a_|_) v ((a ^ b_|_) v a_|_)_|_)
4	3	bi1 110	. . 3 ((((a ^ b_|_) v a_|_)_|_ v ((a ^ b_|_) v a_|_)) == (((a ^ b_|_) v a_|_) v ((a ^ b_|_) v a_|_)_|_)) = 1
5	2, 4	wwbmpr 198	. 2 (((a ^ b_|_) v a_|_)_|_ v ((a ^ b_|_) v a_|_)) = 1
6		df-t 40	. . . . . . . 8 1 = (((a v b_|_) ^ (a v b)) v ((a v b_|_) ^ (a v b))_|_)
7	6	ax-r1 34	. . . . . . 7 (((a v b_|_) ^ (a v b)) v ((a v b_|_) ^ (a v b))_|_) = 1
8	7	bi1 110	. . . . . 6 ((((a v b_|_) ^ (a v b)) v ((a v b_|_) ^ (a v b))_|_) == 1) = 1
9	8	wlan 352	. . . . 5 ((a_|_ ^ (((a v b_|_) ^ (a v b)) v ((a v b_|_) ^ (a v b))_|_)) == (a_|_ ^ 1)) = 1
10		anidm 103	. . . . . . . . . . 11 (a ^ a) = a
11	10	bi1 110	. . . . . . . . . 10 ((a ^ a) == a) = 1
12	11	wr1 189	. . . . . . . . 9 (a == (a ^ a)) = 1
13		wleo 369	. . . . . . . . . 10 (a =<2 (a v b_|_)) = 1
14		wleo 369	. . . . . . . . . 10 (a =<2 (a v b)) = 1
15	13, 14	wle2an 386	. . . . . . . . 9 ((a ^ a) =<2 ((a v b_|_) ^ (a v b))) = 1
16	12, 15	wbltr 379	. . . . . . . 8 (a =<2 ((a v b_|_) ^ (a v b))) = 1
17	16	wlecom 391	. . . . . . 7 C (a, ((a v b_|_) ^ (a v b))) = 1
18	17	wcomcom3 398	. . . . . 6 C (a_|_, ((a v b_|_) ^ (a v b))) = 1
19	17	wcomcom4 399	. . . . . 6 C (a_|_, ((a v b_|_) ^ (a v b))_|_) = 1
20	18, 19	wfh1 405	. . . . 5 ((a_|_ ^ (((a v b_|_) ^ (a v b)) v ((a v b_|_) ^ (a v b))_|_)) == ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a v b_|_) ^ (a v b))_|_))) = 1
21		an1 98	. . . . . 6 (a_|_ ^ 1) = a_|_
22	21	bi1 110	. . . . 5 ((a_|_ ^ 1) == a_|_) = 1
23	9, 20, 22	w3tr2 357	. . . 4 (((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a v b_|_) ^ (a v b))_|_)) == a_|_) = 1
24	23	wlor 350	. . 3 (((a ^ b_|_) v ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a v b_|_) ^ (a v b))_|_))) == ((a ^ b_|_) v a_|_)) = 1
25	24	wlor 350	. 2 ((((a ^ b_|_) v a_|_)_|_ v ((a ^ b_|_) v ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a v b_|_) ^ (a v b))_|_)))) == (((a ^ b_|_) v a_|_)_|_ v ((a ^ b_|_) v a_|_))) = 1
26	5, 25	wwbmpr 198	1 (((a ^ b_|_) v a_|_)_|_ v ((a ^ b_|_) v ((a_|_ ^ ((a v b_|_) ^ (a v b))) v (a_|_ ^ ((a v b_|_) ^ (a v 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-a4 32  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37  ax-wom 343

This theorem depends on definitions:  df-b 38  df-a 39  df-t 40  df-f 41  df-i1 43  df-i2 44  df-le 121  df-le1 122  df-le2 123  df-cmtr 126

metamath.org