Theorem fh2r 456

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 452	. 2 (b ^ (a v c)) = ((b ^ a) v (b ^ c))
4		ancom 68	. 2 ((a v c) ^ b) = (b ^ (a v c))
5		ancom 68	. . 3 (a ^ b) = (b ^ a)
6		ancom 68	. . 3 (c ^ b) = (b ^ c)
7	5, 6	2or 67	. 2 ((a ^ b) v (c ^ b)) = ((b ^ a) v (b ^ c))
8	3, 4, 7	3tr1 60	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 462  ud3lem1a 548  ud3lem2 553  ud3lem3d 557  ud4lem1a 559  ud4lem1b 560  u2lemaa 583  u4lemaa 585  u2lemana 588  u4lemana 590  u1lemab 592  u3lemab 594  u1lemanb 597  u3lemanb 599  u4lemc4 686  u5lemc4 687  u4lem4 741  u24lem 752  bi3 821  bi4 822  marsdenlem1 862  govar 876

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