Theorem fh3 457

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 441	. . . 4 a' C b'
3		fh.2	. . . . 5 a C c
4	3	comcom4 441	. . . 4 a' C c'
5	2, 4	fh1 455	. . 3 (a' ^ (b' v c')) = ((a' ^ b') v (a' ^ c'))
6		anor2 83	. . . 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 67	. . . . 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 81	. . . 4 ((a' ^ b') v (a' ^ c')) = ((a' ^ b')' ^ (a' ^ c')')'
13		oran 81	. . . . . . 7 (a v b) = (a' ^ b')'
14		oran 81	. . . . . . 7 (a v c) = (a' ^ c')'
15	13, 14	2an 73	. . . . . 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 62	. 2 (a v (b ^ c))' = ((a v b) ^ (a v c))'
20	19	con1 64	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 461  i3bi 482  oi3ai3 489  ud1lem2 547  ud1lem3 548  ud2lem3 551  ud3lem1 556  ud4lem1a 563  ud5lem3 580  u4lemob 619  u1lembi 706  u4lem4 745  test 788  3vth5 794  3vth7 796  3vth9 798  1oa 806  2oalem1 811  neg3antlem2 851  comanblem1 856  mhlem 862  gomaex3lem1 900  oau 915  oa23 922  oa3to4lem1 931  oa3to4lem2 932  oa4to6lem1 946  oa4to6lem2 947  oa4to6lem3 948  lem4.6.2e1 1065  lem4.6.6i1j3 1077  com3iia 1085  lem4.6.7 1086

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 425

This theorem depends on definitions:  df-b 39  df-a 40  df-t 41  df-f 42  df-le1 124  df-le2 125  df-c1 126  df-c2 127

Copyright terms: Public domain