Theorem fh4 454

Description: Foulis-Holland Theorem.

Hypotheses

Ref	Expression
fh.1	a C b
fh.2	a C c

Assertion

Ref	Expression
fh4	(b v (a ^ c)) = ((b v a) ^ (b v c))

Proof of Theorem fh4

Step	Hyp	Ref	Expression
1		fh.1	. . . . 5 a C b
2	1	comcom4 437	. . . 4 a_|_ C b_|_
3		fh.2	. . . . 5 a C c
4	3	comcom4 437	. . . 4 a_|_ C c_|_
5	2, 4	fh2 452	. . 3 (b_|_ ^ (a_|_ v c_|_)) = ((b_|_ ^ a_|_) v (b_|_ ^ c_|_))
6		anor2 81	. . . 4 (b_|_ ^ (a_|_ v c_|_)) = (b v (a_|_ v c_|_)_|_)_|_
7		df-a 39	. . . . . . 7 (a ^ c) = (a_|_ v c_|_)_|_
8	7	ax-r1 34	. . . . . 6 (a_|_ v c_|_)_|_ = (a ^ c)
9	8	lor 66	. . . . 5 (b v (a_|_ v c_|_)_|_) = (b v (a ^ c))
10	9	ax-r4 36	. . . 4 (b v (a_|_ v c_|_)_|_)_|_ = (b v (a ^ c))_|_
11	6, 10	ax-r2 35	. . 3 (b_|_ ^ (a_|_ v c_|_)) = (b v (a ^ c))_|_
12		oran 79	. . . 4 ((b_|_ ^ a_|_) v (b_|_ ^ c_|_)) = ((b_|_ ^ a_|_)_|_ ^ (b_|_ ^ c_|_)_|_)_|_
13		oran 79	. . . . . . 7 (b v a) = (b_|_ ^ a_|_)_|_
14		oran 79	. . . . . . 7 (b v c) = (b_|_ ^ c_|_)_|_
15	13, 14	2an 72	. . . . . 6 ((b v a) ^ (b v c)) = ((b_|_ ^ a_|_)_|_ ^ (b_|_ ^ c_|_)_|_)
16	15	ax-r1 34	. . . . 5 ((b_|_ ^ a_|_)_|_ ^ (b_|_ ^ c_|_)_|_) = ((b v a) ^ (b v c))
17	16	ax-r4 36	. . . 4 ((b_|_ ^ a_|_)_|_ ^ (b_|_ ^ c_|_)_|_)_|_ = ((b v a) ^ (b v c))_|_
18	12, 17	ax-r2 35	. . 3 ((b_|_ ^ a_|_) v (b_|_ ^ c_|_)) = ((b v a) ^ (b v c))_|_
19	5, 11, 18	3tr2 61	. 2 (b v (a ^ c))_|_ = ((b v a) ^ (b v c))_|_
20	19	con1 63	1 (b v (a ^ c)) = ((b v a) ^ (b v c))

Syntax hints:   = wb 1   C wc 3  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  fh4r 458  fh4c 460  df2i3 480  i3abs3 506  i3con 533  ud3lem1c 550  ud4lem1c 561  ud4lem1 563  ud5lem1 571  ud5lem3 576  u5lemaa 586  u4lemona 610  u3lemob 614  u3lemonb 619  u1lemc4 683  u2lemc4 684  u3lemc4 685  u4lemc4 686  u5lemc4 687  u4lem1 719  u2lem3 732  u1lem4 739  u4lem5 746  u5lem5 747  u4lem6 750  u5lem6 751  u3lem11 768  orbi 824

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-r3 421

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