Theorem fh3 453

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

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

Proof of Theorem fh3

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	fh1 451	. . 3 (a_|_ ^ (b_|_ v c_|_)) = ((a_|_ ^ b_|_) v (a_|_ ^ c_|_))
6		anor2 81	. . . 4 (a_|_ ^ (b_|_ v c_|_)) = (a v (b_|_ v c_|_)_|_)_|_
7		df-a 39	. . . . . . 7 (b ^ c) = (b_|_ v c_|_)_|_
8	7	ax-r1 34	. . . . . 6 (b_|_ v c_|_)_|_ = (b ^ c)
9	8	lor 66	. . . . 5 (a v (b_|_ v c_|_)_|_) = (a v (b ^ c))
10	9	ax-r4 36	. . . 4 (a v (b_|_ v c_|_)_|_)_|_ = (a v (b ^ c))_|_
11	6, 10	ax-r2 35	. . 3 (a_|_ ^ (b_|_ v c_|_)) = (a v (b ^ c))_|_
12		oran 79	. . . 4 ((a_|_ ^ b_|_) v (a_|_ ^ c_|_)) = ((a_|_ ^ b_|_)_|_ ^ (a_|_ ^ c_|_)_|_)_|_
13		oran 79	. . . . . . 7 (a v b) = (a_|_ ^ b_|_)_|_
14		oran 79	. . . . . . 7 (a v c) = (a_|_ ^ c_|_)_|_
15	13, 14	2an 72	. . . . . 6 ((a v b) ^ (a v c)) = ((a_|_ ^ b_|_)_|_ ^ (a_|_ ^ c_|_)_|_)
16	15	ax-r1 34	. . . . 5 ((a_|_ ^ b_|_)_|_ ^ (a_|_ ^ c_|_)_|_) = ((a v b) ^ (a v c))
17	16	ax-r4 36	. . . 4 ((a_|_ ^ b_|_)_|_ ^ (a_|_ ^ c_|_)_|_)_|_ = ((a v b) ^ (a v c))_|_
18	12, 17	ax-r2 35	. . 3 ((a_|_ ^ b_|_) v (a_|_ ^ c_|_)) = ((a v b) ^ (a v c))_|_
19	5, 11, 18	3tr2 61	. 2 (a v (b ^ c))_|_ = ((a v b) ^ (a v c))_|_
20	19	con1 63	1 (a v (b ^ c)) = ((a v b) ^ (a v c))

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

This theorem is referenced by:  fh3r 457  i3bi 478  oi3ai3 485  ud1lem2 543  ud1lem3 544  ud2lem3 547  ud3lem1 552  ud4lem1a 559  ud5lem3 576  u4lemob 615  u1lembi 702  u4lem4 741  test 784  3vth5 790  3vth7 792  3vth9 794  1oa 802  2oalem1 807  neg3antlem2 847  comanblem1 852  mhlem 858  gomaex3lem1 894  oau 909  oa23 916  oa3to4lem1 925  oa3to4lem2 926  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942

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