Theorem woml7 419

Description: Variant of weakly orthomodular law.

Assertion

Ref	Expression
woml7	(((a ->2 b) ^ (b ->2 a))_|_ v (a == b)) = 1

Proof of Theorem woml7

Step	Hyp	Ref	Expression
1		df-i2 44	. . . . . . . 8 (a ->2 b) = (b v (a_|_ ^ b_|_))
2		ax-a2 30	. . . . . . . 8 (b v (a_|_ ^ b_|_)) = ((a_|_ ^ b_|_) v b)
3	1, 2	ax-r2 35	. . . . . . 7 (a ->2 b) = ((a_|_ ^ b_|_) v b)
4		df-i2 44	. . . . . . . 8 (b ->2 a) = (a v (b_|_ ^ a_|_))
5		ax-a2 30	. . . . . . . 8 (a v (b_|_ ^ a_|_)) = ((b_|_ ^ a_|_) v a)
6		ancom 68	. . . . . . . . 9 (b_|_ ^ a_|_) = (a_|_ ^ b_|_)
7	6	ax-r5 37	. . . . . . . 8 ((b_|_ ^ a_|_) v a) = ((a_|_ ^ b_|_) v a)
8	4, 5, 7	3tr 62	. . . . . . 7 (b ->2 a) = ((a_|_ ^ b_|_) v a)
9	3, 8	2an 72	. . . . . 6 ((a ->2 b) ^ (b ->2 a)) = (((a_|_ ^ b_|_) v b) ^ ((a_|_ ^ b_|_) v a))
10		ancom 68	. . . . . 6 (((a_|_ ^ b_|_) v b) ^ ((a_|_ ^ b_|_) v a)) = (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))
11	9, 10	ax-r2 35	. . . . 5 ((a ->2 b) ^ (b ->2 a)) = (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))
12	11	ax-r4 36	. . . 4 ((a ->2 b) ^ (b ->2 a))_|_ = (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_
13		id 58	. . . 4 (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_ = (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_
14	12, 13	ax-r2 35	. . 3 ((a ->2 b) ^ (b ->2 a))_|_ = (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_
15		dfb 86	. . 3 (a == b) = ((a ^ b) v (a_|_ ^ b_|_))
16	14, 15	2or 67	. 2 (((a ->2 b) ^ (b ->2 a))_|_ v (a == b)) = ((((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_ v ((a ^ b) v (a_|_ ^ b_|_)))
17		1b 109	. . 3 (1 == ((((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_ v ((a ^ b) v (a_|_ ^ b_|_)))) = ((((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_ v ((a ^ b) v (a_|_ ^ b_|_)))
18	17	ax-r1 34	. 2 ((((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_ v ((a ^ b) v (a_|_ ^ b_|_))) = (1 == ((((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_ v ((a ^ b) v (a_|_ ^ b_|_))))
19		df-t 40	. . . . 5 1 = (((a ^ b) v (a_|_ ^ b_|_)) v ((a ^ b) v (a_|_ ^ b_|_))_|_)
20		ax-a2 30	. . . . 5 (((a ^ b) v (a_|_ ^ b_|_)) v ((a ^ b) v (a_|_ ^ b_|_))_|_) = (((a ^ b) v (a_|_ ^ b_|_))_|_ v ((a ^ b) v (a_|_ ^ b_|_)))
21	19, 20	ax-r2 35	. . . 4 1 = (((a ^ b) v (a_|_ ^ b_|_))_|_ v ((a ^ b) v (a_|_ ^ b_|_)))
22	21	bi1 110	. . 3 (1 == (((a ^ b) v (a_|_ ^ b_|_))_|_ v ((a ^ b) v (a_|_ ^ b_|_)))) = 1
23		wa2 184	. . . . . 6 (((a ^ b) v (a_|_ ^ b_|_)) == ((a_|_ ^ b_|_) v (a ^ b))) = 1
24		wcoman1 395	. . . . . . . . 9 C ((a_|_ ^ b_|_), a_|_) = 1
25	24	wcomcom3 398	. . . . . . . 8 C ((a_|_ ^ b_|_)_|_, a_|_) = 1
26	25	wcomcom5 402	. . . . . . 7 C ((a_|_ ^ b_|_), a) = 1
27		ancom 68	. . . . . . . . . . 11 (a_|_ ^ b_|_) = (b_|_ ^ a_|_)
28	27	bi1 110	. . . . . . . . . 10 ((a_|_ ^ b_|_) == (b_|_ ^ a_|_)) = 1
29		wcoman1 395	. . . . . . . . . 10 C ((b_|_ ^ a_|_), b_|_) = 1
30	28, 29	wbctr 392	. . . . . . . . 9 C ((a_|_ ^ b_|_), b_|_) = 1
31	30	wcomcom3 398	. . . . . . . 8 C ((a_|_ ^ b_|_)_|_, b_|_) = 1
32	31	wcomcom5 402	. . . . . . 7 C ((a_|_ ^ b_|_), b) = 1
33	26, 32	wfh3 407	. . . . . 6 (((a_|_ ^ b_|_) v (a ^ b)) == (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))) = 1
34	23, 33	wr2 353	. . . . 5 (((a ^ b) v (a_|_ ^ b_|_)) == (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))) = 1
35	34	wr4 191	. . . 4 (((a ^ b) v (a_|_ ^ b_|_))_|_ == (((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_) = 1
36	35	wr5-2v 348	. . 3 ((((a ^ b) v (a_|_ ^ b_|_))_|_ v ((a ^ b) v (a_|_ ^ b_|_))) == ((((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_ v ((a ^ b) v (a_|_ ^ b_|_)))) = 1
37	22, 36	wr2 353	. 2 (1 == ((((a_|_ ^ b_|_) v a) ^ ((a_|_ ^ b_|_) v b))_|_ v ((a ^ b) v (a_|_ ^ b_|_)))) = 1
38	16, 18, 37	3tr 62	1 (((a ->2 b) ^ (b ->2 a))_|_ v (a == b)) = 1

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

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