Theorem com2or 465

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 435	. . . . . . . 8 b C a
3	2	df-c2 125	. . . . . . 7 b = ((b ^ a) v (b ^ a_|_))
4		ancom 68	. . . . . . . 8 (b ^ a) = (a ^ b)
5		ancom 68	. . . . . . . 8 (b ^ a_|_) = (a_|_ ^ b)
6	4, 5	2or 67	. . . . . . 7 ((b ^ a) v (b ^ a_|_)) = ((a ^ b) v (a_|_ ^ b))
7	3, 6	ax-r2 35	. . . . . 6 b = ((a ^ b) v (a_|_ ^ b))
8		fh.2	. . . . . . . . 9 a C c
9	8	comcom 435	. . . . . . . 8 c C a
10	9	df-c2 125	. . . . . . 7 c = ((c ^ a) v (c ^ a_|_))
11		ancom 68	. . . . . . . 8 (c ^ a) = (a ^ c)
12		ancom 68	. . . . . . . 8 (c ^ a_|_) = (a_|_ ^ c)
13	11, 12	2or 67	. . . . . . 7 ((c ^ a) v (c ^ a_|_)) = ((a ^ c) v (a_|_ ^ c))
14	10, 13	ax-r2 35	. . . . . 6 c = ((a ^ c) v (a_|_ ^ c))
15	7, 14	2or 67	. . . . 5 (b v c) = (((a ^ b) v (a_|_ ^ b)) v ((a ^ c) v (a_|_ ^ c)))
16		or4 77	. . . . 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 35	. . . 4 (b v c) = (((a ^ b) v (a ^ c)) v ((a_|_ ^ b) v (a_|_ ^ c)))
18		ancom 68	. . . . . . 7 ((b v c) ^ a) = (a ^ (b v c))
19	1, 8	fh1 451	. . . . . . 7 (a ^ (b v c)) = ((a ^ b) v (a ^ c))
20	18, 19	ax-r2 35	. . . . . 6 ((b v c) ^ a) = ((a ^ b) v (a ^ c))
21		ancom 68	. . . . . . 7 ((b v c) ^ a_|_) = (a_|_ ^ (b v c))
22	1	comcom3 436	. . . . . . . 8 a_|_ C b
23	8	comcom3 436	. . . . . . . 8 a_|_ C c
24	22, 23	fh1 451	. . . . . . 7 (a_|_ ^ (b v c)) = ((a_|_ ^ b) v (a_|_ ^ c))
25	21, 24	ax-r2 35	. . . . . 6 ((b v c) ^ a_|_) = ((a_|_ ^ b) v (a_|_ ^ c))
26	20, 25	2or 67	. . . . 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 34	. . . 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 35	. . 3 (b v c) = (((b v c) ^ a) v ((b v c) ^ a_|_))
29	28	df-c1 124	. 2 (b v c) C a
30	29	comcom 435	1 a C (b v c)

Syntax hints:   C wc 3  _|_wn 4   v wo 6   ^ wa 7

This theorem is referenced by:  com2an 466  combi 467  gsth 471  gsth2 472  gt1 474  dfi3b 481  oi3ai3 485  comi31 490  com2i3 491  i3con 533  i3orlem7 540  i3orlem8 541  ud1lem3 544  ud3lem1a 548  ud3lem1c 550  ud3lem1d 551  ud3lem1 552  ud3lem3d 557  ud3lem3 558  ud4lem1a 559  ud4lem1b 560  ud4lem1c 561  ud4lem1 563  ud4lem3b 566  ud4lem3 567  ud5lem1a 568  ud5lem1b 569  ud5lem1 571  ud5lem3a 573  ud5lem3 576  u3lemaa 584  u4lemaa 585  u5lemaa 586  u3lemana 589  u4lemana 590  u5lemana 591  u3lemab 594  u4lemab 595  u5lemab 596  u3lemanb 599  u4lemanb 600  u5lemanb 601  u4lemona 610  u3lemob 614  u3lemonb 619  u1lemc1 662  u2lemc1 663  u4lemc1 665  u5lemc1 666  u5lemc1b 667  u1lemc2 668  u2lemc2 669  u4lemc2 671  u5lemc2 672  u4lemle2 700  u5lemle2 701  u5lembi 707  u4lem1 719  u4lem4 741  u4lem5 746  u4lem6 750  u24lem 752  u1lem8 758  u1lem11 762  u3lem13a 771  u3lem13b 772  u3lem15 777  test 784  test2 785  3vded21 799  mlalem 814  mlaconj4 826  neg3antlem2 847  mhlem 858  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