Theorem fh4r 458

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

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

Proof of Theorem fh4r

Step	Hyp	Ref	Expression
1		fh.1	. . 3 a C b
2		fh.2	. . 3 a C c
3	1, 2	fh4 454	. 2 (b v (a ^ c)) = ((b v a) ^ (b v c))
4		ax-a2 30	. 2 ((a ^ c) v b) = (b v (a ^ c))
5		ax-a2 30	. . 3 (a v b) = (b v a)
6		ax-a2 30	. . 3 (c v b) = (b v c)
7	5, 6	2an 72	. 2 ((a v b) ^ (c v b)) = ((b v a) ^ (b v c))
8	3, 4, 7	3tr1 60	1 ((a ^ c) v b) = ((a v b) ^ (c v b))

Syntax hints:   = wb 1   C wc 3   v wo 6   ^ wa 7

This theorem is referenced by:  fh4rc 464  ud1lem1 542  ud1lem3 544  ud3lem1c 550  ud3lem3 558  ud4lem1c 561  ud4lem3 567  u4lemoa 605  u24lem 752  u3lem10 767  u3lem13a 771  u3lem13b 772  i1abs 783  test 784  test2 785

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