Theorem wwfh4 211

Description: Foulis-Holland Theorem (weak).

Hypotheses

Ref	Expression
wwfh4.1	a_|_ C b
wwfh4.2	c C a

Assertion

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

Proof of Theorem wwfh4

Step	Hyp	Ref	Expression
1		conb 114	. . 3 ((b v (a ^ c)) == ((b v a) ^ (b v c))) = ((b v (a ^ c))_|_ == ((b v a) ^ (b v c))_|_)
2		oran 79	. . . . . 6 (b v (a ^ c)) = (b_|_ ^ (a ^ c)_|_)_|_
3		df-a 39	. . . . . . . . 9 (a ^ c) = (a_|_ v c_|_)_|_
4	3	con2 64	. . . . . . . 8 (a ^ c)_|_ = (a_|_ v c_|_)
5	4	lan 70	. . . . . . 7 (b_|_ ^ (a ^ c)_|_) = (b_|_ ^ (a_|_ v c_|_))
6	5	ax-r4 36	. . . . . 6 (b_|_ ^ (a ^ c)_|_)_|_ = (b_|_ ^ (a_|_ v c_|_))_|_
7	2, 6	ax-r2 35	. . . . 5 (b v (a ^ c)) = (b_|_ ^ (a_|_ v c_|_))_|_
8	7	con2 64	. . . 4 (b v (a ^ c))_|_ = (b_|_ ^ (a_|_ v c_|_))
9		df-a 39	. . . . . 6 ((b v a) ^ (b v c)) = ((b v a)_|_ v (b v c)_|_)_|_
10		oran 79	. . . . . . . . 9 (b v a) = (b_|_ ^ a_|_)_|_
11	10	con2 64	. . . . . . . 8 (b v a)_|_ = (b_|_ ^ a_|_)
12		oran 79	. . . . . . . . 9 (b v c) = (b_|_ ^ c_|_)_|_
13	12	con2 64	. . . . . . . 8 (b v c)_|_ = (b_|_ ^ c_|_)
14	11, 13	2or 67	. . . . . . 7 ((b v a)_|_ v (b v c)_|_) = ((b_|_ ^ a_|_) v (b_|_ ^ c_|_))
15	14	ax-r4 36	. . . . . 6 ((b v a)_|_ v (b v c)_|_)_|_ = ((b_|_ ^ a_|_) v (b_|_ ^ c_|_))_|_
16	9, 15	ax-r2 35	. . . . 5 ((b v a) ^ (b v c)) = ((b_|_ ^ a_|_) v (b_|_ ^ c_|_))_|_
17	16	con2 64	. . . 4 ((b v a) ^ (b v c))_|_ = ((b_|_ ^ a_|_) v (b_|_ ^ c_|_))
18	8, 17	2bi 91	. . 3 ((b v (a ^ c))_|_ == ((b v a) ^ (b v c))_|_) = ((b_|_ ^ (a_|_ v c_|_)) == ((b_|_ ^ a_|_) v (b_|_ ^ c_|_)))
19	1, 18	ax-r2 35	. 2 ((b v (a ^ c)) == ((b v a) ^ (b v c))) = ((b_|_ ^ (a_|_ v c_|_)) == ((b_|_ ^ a_|_) v (b_|_ ^ c_|_)))
20		wwfh4.1	. . . 4 a_|_ C b
21	20	comcom2 175	. . 3 a_|_ C b_|_
22		ax-a1 29	. . . . . 6 c = c_|__|_
23	22	ax-r1 34	. . . . 5 c_|__|_ = c
24		wwfh4.2	. . . . 5 c C a
25	23, 24	bctr 173	. . . 4 c_|__|_ C a
26	25	comcom2 175	. . 3 c_|__|_ C a_|_
27	21, 26	wwfh2 209	. 2 ((b_|_ ^ (a_|_ v c_|_)) == ((b_|_ ^ a_|_) v (b_|_ ^ c_|_))) = 1
28	19, 27	ax-r2 35	1 ((b v (a ^ c)) == ((b v a) ^ (b 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