Theorem fh2r 474

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

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

Proof of Theorem fh2r

Step	Hyp	Ref	Expression
1		fh.1	. . 3 a C b
2		fh.2	. . 3 a C c
3	1, 2	fh2 470	. 2 (b ^ (a v c)) = ((b ^ a) v (b ^ c))
4		ancom 74	. 2 ((a v c) ^ b) = (b ^ (a v c))
5		ancom 74	. . 3 (a ^ b) = (b ^ a)
6		ancom 74	. . 3 (c ^ b) = (b ^ c)
7	5, 6	2or 72	. 2 ((a ^ b) v (c ^ b)) = ((b ^ a) v (b ^ c))
8	3, 4, 7	3tr1 63	1 ((a v c) ^ b) = ((a ^ b) v (c ^ b))

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

This theorem is referenced by:  fh2rc 480  ud3lem1a 566  ud3lem2 571  ud3lem3d 575  ud4lem1a 577  ud4lem1b 578  u2lemaa 601  u4lemaa 603  u2lemana 606  u4lemana 608  u1lemab 610  u3lemab 612  u1lemanb 615  u3lemanb 617  u4lemc4 704  u5lemc4 705  u4lem4 759  u24lem 770  bi3 839  bi4 840  marsdenlem1 880  e2astlem1 895  govar 896

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