Theorem wwfh3 210

Description: Foulis-Holland Theorem (weak).

Hypotheses

Ref	Expression
wwfh3.1	b_|_ C a
wwfh3.2	c_|_ C a

Assertion

Ref	Expression
wwfh3	((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1

Proof of Theorem wwfh3

Step	Hyp	Ref	Expression
1		conb 114	. . 3 ((a v (b ^ c)) == ((a v b) ^ (a v c))) = ((a v (b ^ c))_|_ == ((a v b) ^ (a v c))_|_)
2		oran 79	. . . . . 6 (a v (b ^ c)) = (a_|_ ^ (b ^ c)_|_)_|_
3		df-a 39	. . . . . . . . 9 (b ^ c) = (b_|_ v c_|_)_|_
4	3	con2 64	. . . . . . . 8 (b ^ c)_|_ = (b_|_ v c_|_)
5	4	lan 70	. . . . . . 7 (a_|_ ^ (b ^ c)_|_) = (a_|_ ^ (b_|_ v c_|_))
6	5	ax-r4 36	. . . . . 6 (a_|_ ^ (b ^ c)_|_)_|_ = (a_|_ ^ (b_|_ v c_|_))_|_
7	2, 6	ax-r2 35	. . . . 5 (a v (b ^ c)) = (a_|_ ^ (b_|_ v c_|_))_|_
8	7	con2 64	. . . 4 (a v (b ^ c))_|_ = (a_|_ ^ (b_|_ v c_|_))
9		df-a 39	. . . . . 6 ((a v b) ^ (a v c)) = ((a v b)_|_ v (a v c)_|_)_|_
10		oran 79	. . . . . . . . 9 (a v b) = (a_|_ ^ b_|_)_|_
11	10	con2 64	. . . . . . . 8 (a v b)_|_ = (a_|_ ^ b_|_)
12		oran 79	. . . . . . . . 9 (a v c) = (a_|_ ^ c_|_)_|_
13	12	con2 64	. . . . . . . 8 (a v c)_|_ = (a_|_ ^ c_|_)
14	11, 13	2or 67	. . . . . . 7 ((a v b)_|_ v (a v c)_|_) = ((a_|_ ^ b_|_) v (a_|_ ^ c_|_))
15	14	ax-r4 36	. . . . . 6 ((a v b)_|_ v (a v c)_|_)_|_ = ((a_|_ ^ b_|_) v (a_|_ ^ c_|_))_|_
16	9, 15	ax-r2 35	. . . . 5 ((a v b) ^ (a v c)) = ((a_|_ ^ b_|_) v (a_|_ ^ c_|_))_|_
17	16	con2 64	. . . 4 ((a v b) ^ (a v c))_|_ = ((a_|_ ^ b_|_) v (a_|_ ^ c_|_))
18	8, 17	2bi 91	. . 3 ((a v (b ^ c))_|_ == ((a v b) ^ (a v c))_|_) = ((a_|_ ^ (b_|_ v c_|_)) == ((a_|_ ^ b_|_) v (a_|_ ^ c_|_)))
19	1, 18	ax-r2 35	. 2 ((a v (b ^ c)) == ((a v b) ^ (a v c))) = ((a_|_ ^ (b_|_ v c_|_)) == ((a_|_ ^ b_|_) v (a_|_ ^ c_|_)))
20		wwfh3.1	. . . 4 b_|_ C a
21	20	comcom2 175	. . 3 b_|_ C a_|_
22		wwfh3.2	. . . 4 c_|_ C a
23	22	comcom2 175	. . 3 c_|_ C a_|_
24	21, 23	wwfh1 208	. 2 ((a_|_ ^ (b_|_ v c_|_)) == ((a_|_ ^ b_|_) v (a_|_ ^ c_|_))) = 1
25	19, 24	ax-r2 35	1 ((a v (b ^ c)) == ((a v b) ^ (a v c))) = 1

Syntax hints:   = wb 1   C wc 3  _|_wn 4   == tb 5   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

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