Theorem com2or 483

Description: Th. 4.2 Beran p. 49.

Hypotheses

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

Assertion

Ref	Expression
com2or	a C (b v c)

Proof of Theorem com2or

Step	Hyp	Ref	Expression
1		fh.1	. . . . . . . . 9 a C b
2	1	comcom 453	. . . . . . . 8 b C a
3	2	df-c2 133	. . . . . . 7 b = ((b ^ a) v (b ^ a'))
4		ancom 74	. . . . . . . 8 (b ^ a) = (a ^ b)
5		ancom 74	. . . . . . . 8 (b ^ a') = (a' ^ b)
6	4, 5	2or 72	. . . . . . 7 ((b ^ a) v (b ^ a')) = ((a ^ b) v (a' ^ b))
7	3, 6	ax-r2 36	. . . . . 6 b = ((a ^ b) v (a' ^ b))
8		fh.2	. . . . . . . . 9 a C c
9	8	comcom 453	. . . . . . . 8 c C a
10	9	df-c2 133	. . . . . . 7 c = ((c ^ a) v (c ^ a'))
11		ancom 74	. . . . . . . 8 (c ^ a) = (a ^ c)
12		ancom 74	. . . . . . . 8 (c ^ a') = (a' ^ c)
13	11, 12	2or 72	. . . . . . 7 ((c ^ a) v (c ^ a')) = ((a ^ c) v (a' ^ c))
14	10, 13	ax-r2 36	. . . . . 6 c = ((a ^ c) v (a' ^ c))
15	7, 14	2or 72	. . . . 5 (b v c) = (((a ^ b) v (a' ^ b)) v ((a ^ c) v (a' ^ c)))
16		or4 84	. . . . 5 (((a ^ b) v (a' ^ b)) v ((a ^ c) v (a' ^ c))) = (((a ^ b) v (a ^ c)) v ((a' ^ b) v (a' ^ c)))
17	15, 16	ax-r2 36	. . . 4 (b v c) = (((a ^ b) v (a ^ c)) v ((a' ^ b) v (a' ^ c)))
18		ancom 74	. . . . . . 7 ((b v c) ^ a) = (a ^ (b v c))
19	1, 8	fh1 469	. . . . . . 7 (a ^ (b v c)) = ((a ^ b) v (a ^ c))
20	18, 19	ax-r2 36	. . . . . 6 ((b v c) ^ a) = ((a ^ b) v (a ^ c))
21		ancom 74	. . . . . . 7 ((b v c) ^ a') = (a' ^ (b v c))
22	1	comcom3 454	. . . . . . . 8 a' C b
23	8	comcom3 454	. . . . . . . 8 a' C c
24	22, 23	fh1 469	. . . . . . 7 (a' ^ (b v c)) = ((a' ^ b) v (a' ^ c))
25	21, 24	ax-r2 36	. . . . . 6 ((b v c) ^ a') = ((a' ^ b) v (a' ^ c))
26	20, 25	2or 72	. . . . 5 (((b v c) ^ a) v ((b v c) ^ a')) = (((a ^ b) v (a ^ c)) v ((a' ^ b) v (a' ^ c)))
27	26	ax-r1 35	. . . 4 (((a ^ b) v (a ^ c)) v ((a' ^ b) v (a' ^ c))) = (((b v c) ^ a) v ((b v c) ^ a'))
28	17, 27	ax-r2 36	. . 3 (b v c) = (((b v c) ^ a) v ((b v c) ^ a'))
29	28	df-c1 132	. 2 (b v c) C a
30	29	comcom 453	1 a C (b v c)

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

This theorem is referenced by:  com2an 484  combi 485  gsth 489  gsth2 490  gt1 492  dfi3b 499  oi3ai3 503  comi31 508  com2i3 509  i3con 551  i3orlem7 558  i3orlem8 559  ud1lem3 562  ud3lem1a 566  ud3lem1c 568  ud3lem1d 569  ud3lem1 570  ud3lem3d 575  ud3lem3 576  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud4lem1 581  ud4lem3b 584  ud4lem3 585  ud5lem1a 586  ud5lem1b 587  ud5lem1 589  ud5lem3a 591  ud5lem3 594  u3lemaa 602  u4lemaa 603  u5lemaa 604  u3lemana 607  u4lemana 608  u5lemana 609  u3lemab 612  u4lemab 613  u5lemab 614  u3lemanb 617  u4lemanb 618  u5lemanb 619  u4lemona 628  u3lemob 632  u3lemonb 637  u1lemc1 680  u2lemc1 681  u4lemc1 683  u5lemc1 684  u5lemc1b 685  u1lemc2 686  u2lemc2 687  u4lemc2 689  u5lemc2 690  u4lemle2 718  u5lemle2 719  u5lembi 725  u4lem1 737  u4lem4 759  u4lem5 764  u4lem6 768  u24lem 770  u1lem8 776  u1lem11 780  u3lem13a 789  u3lem13b 790  u3lem15 795  test 802  test2 803  3vded21 817  mlalem 832  mlaconj4 844  neg3antlem2 865  mhlem 876  e2ast2 894  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