Theorem fh4r 476

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 472	. 2 (b v (a ^ c)) = ((b v a) ^ (b v c))
4		ax-a2 31	. 2 ((a ^ c) v b) = (b v (a ^ c))
5		ax-a2 31	. . 3 (a v b) = (b v a)
6		ax-a2 31	. . 3 (c v b) = (b v c)
7	5, 6	2an 79	. 2 ((a v b) ^ (c v b)) = ((b v a) ^ (b v c))
8	3, 4, 7	3tr1 63	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 482  ud1lem1 560  ud1lem3 562  ud3lem1c 568  ud3lem3 576  ud4lem1c 579  ud4lem3 585  u4lemoa 623  u24lem 770  u3lem10 785  u3lem13a 789  u3lem13b 790  i1abs 801  test 802  test2 803

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a4 33  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38  ax-r3 439

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 130  df-le2 131  df-c1 132  df-c2 133

Copyright terms: Public domain