Theorem fh1r 455

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

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

Proof of Theorem fh1r

Step	Hyp	Ref	Expression
1		fh.1	. . 3 a C b
2		fh.2	. . 3 a C c
3	1, 2	fh1 451	. 2 (a ^ (b v c)) = ((a ^ b) v (a ^ c))
4		ancom 68	. 2 ((b v c) ^ a) = (a ^ (b v c))
5		ancom 68	. . 3 (b ^ a) = (a ^ b)
6		ancom 68	. . 3 (c ^ a) = (a ^ c)
7	5, 6	2or 67	. 2 ((b ^ a) v (c ^ a)) = ((a ^ b) v (a ^ c))
8	3, 4, 7	3tr1 60	1 ((b v c) ^ a) = ((b ^ a) v (c ^ a))

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

This theorem is referenced by:  fh1rc 461  gsth 471  dfi3b 481  ud3lem1b 549  ud3lem1d 551  ud3lem3d 557  ud5lem1a 568  ud5lem3a 573  u1lemaa 582  u3lemaa 584  u4lemaa 585  u5lemaa 586  u3lemana 589  u4lemana 590  u5lemana 591  u3lemab 594  u4lemab 595  u5lemab 596  u2lemanb 598  u4lemanb 600  u5lemanb 601  u4lem4 741  u4lem5 746  u5lem5 747  u5lem6 751  u1lem8 758  u3lem15 777  bi1o1a 780  3vded21 799  1oa 802  neg3antlem2 847  mhlem 858  mhlem1 859  marsdenlem3 864  marsdenlem4 865

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