Theorem fh3 471

Description: Foulis-Holland Theorem.

Hypotheses

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

Assertion

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

Proof of Theorem fh3

Step	Hyp	Ref	Expression
1		fh.1	. . . . 5 a C b
2	1	comcom4 455	. . . 4 a' C b'
3		fh.2	. . . . 5 a C c
4	3	comcom4 455	. . . 4 a' C c'
5	2, 4	fh1 469	. . 3 (a' ^ (b' v c')) = ((a' ^ b') v (a' ^ c'))
6		anor2 89	. . . 4 (a' ^ (b' v c')) = (a v (b' v c')')'
7		df-a 40	. . . . . . 7 (b ^ c) = (b' v c')'
8	7	ax-r1 35	. . . . . 6 (b' v c')' = (b ^ c)
9	8	lor 70	. . . . 5 (a v (b' v c')') = (a v (b ^ c))
10	9	ax-r4 37	. . . 4 (a v (b' v c')')' = (a v (b ^ c))'
11	6, 10	ax-r2 36	. . 3 (a' ^ (b' v c')) = (a v (b ^ c))'
12		oran 87	. . . 4 ((a' ^ b') v (a' ^ c')) = ((a' ^ b')' ^ (a' ^ c')')'
13		oran 87	. . . . . . 7 (a v b) = (a' ^ b')'
14		oran 87	. . . . . . 7 (a v c) = (a' ^ c')'
15	13, 14	2an 79	. . . . . 6 ((a v b) ^ (a v c)) = ((a' ^ b')' ^ (a' ^ c')')
16	15	ax-r1 35	. . . . 5 ((a' ^ b')' ^ (a' ^ c')') = ((a v b) ^ (a v c))
17	16	ax-r4 37	. . . 4 ((a' ^ b')' ^ (a' ^ c')')' = ((a v b) ^ (a v c))'
18	12, 17	ax-r2 36	. . 3 ((a' ^ b') v (a' ^ c')) = ((a v b) ^ (a v c))'
19	5, 11, 18	3tr2 64	. 2 (a v (b ^ c))' = ((a v b) ^ (a v c))'
20	19	con1 66	1 (a v (b ^ c)) = ((a v b) ^ (a v c))

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

This theorem is referenced by:  fh3r 475  i3bi 496  oi3ai3 503  ud1lem2 561  ud1lem3 562  ud2lem3 565  ud3lem1 570  ud4lem1a 577  ud5lem3 594  u4lemob 633  u1lembi 720  u4lem4 759  test 802  3vth5 808  3vth7 810  3vth9 812  1oa 820  2oalem1 825  neg3antlem2 865  comanblem1 870  mhlem 876  gomaex3lem1 914  oau 929  oa23 936  oa3to4lem1 945  oa3to4lem2 946  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  lem4.6.2e1 1079  lem4.6.6i1j3 1091  com3iia 1099  lem4.6.7 1100

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