Theorem gsth2 476

Description: Stronger version of Gudder-Schelp's Theorem. Beran, p. 263, Th. 4.2.

Hypotheses

Ref	Expression
gsth2.1	b C c
gsth2.2	a C (b ^ c)

Assertion

Ref	Expression
gsth2	(a ^ b) C c

Proof of Theorem gsth2

Step	Hyp	Ref	Expression
1		gsth2.1	. . . . 5 b C c
2	1	comcom 439	. . . 4 c C b
3		ancom 69	. . . . . . . . 9 (b ^ (b' v a')) = ((b' v a') ^ b)
4		ax-a2 31	. . . . . . . . . 10 (b' v a') = (a' v b')
5	4	ran 72	. . . . . . . . 9 ((b' v a') ^ b) = ((a' v b') ^ b)
6	3, 5	ax-r2 36	. . . . . . . 8 (b ^ (b' v a')) = ((a' v b') ^ b)
7		comor2 448	. . . . . . . . . 10 (a' v b') C b'
8	7	comcom7 446	. . . . . . . . 9 (a' v b') C b
9		gsth2.2	. . . . . . . . . . . . 13 a C (b ^ c)
10	9	comcom 439	. . . . . . . . . . . 12 (b ^ c) C a
11	10	comcom2 177	. . . . . . . . . . 11 (b ^ c) C a'
12		coman1 179	. . . . . . . . . . . 12 (b ^ c) C b
13	12	comcom2 177	. . . . . . . . . . 11 (b ^ c) C b'
14	11, 13	com2or 469	. . . . . . . . . 10 (b ^ c) C (a' v b')
15	14	comcom 439	. . . . . . . . 9 (a' v b') C (b ^ c)
16	8, 1, 15	gsth 475	. . . . . . . 8 ((a' v b') ^ b) C c
17	6, 16	bctr 175	. . . . . . 7 (b ^ (b' v a')) C c
18	17	comcom 439	. . . . . 6 c C (b ^ (b' v a'))
19		df-a 40	. . . . . . 7 (b ^ (b' v a')) = (b' v (b' v a')')'
20		df-a 40	. . . . . . . . . 10 (b ^ a) = (b' v a')'
21	20	lor 67	. . . . . . . . 9 (b' v (b ^ a)) = (b' v (b' v a')')
22	21	ax-r4 37	. . . . . . . 8 (b' v (b ^ a))' = (b' v (b' v a')')'
23	22	ax-r1 35	. . . . . . 7 (b' v (b' v a')')' = (b' v (b ^ a))'
24	19, 23	ax-r2 36	. . . . . 6 (b ^ (b' v a')) = (b' v (b ^ a))'
25	18, 24	cbtr 176	. . . . 5 c C (b' v (b ^ a))'
26	25	comcom7 446	. . . 4 c C (b' v (b ^ a))
27	2, 26	com2an 470	. . 3 c C (b ^ (b' v (b ^ a)))
28		omla 433	. . . 4 (b ^ (b' v (b ^ a))) = (b ^ a)
29		ancom 69	. . . 4 (b ^ a) = (a ^ b)
30	28, 29	ax-r2 36	. . 3 (b ^ (b' v (b ^ a))) = (a ^ b)
31	27, 30	cbtr 176	. 2 c C (a ^ b)
32	31	comcom 439	1 (a ^ b) C c

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

This theorem is referenced by:  gstho 477  oacom 997  oacom3 999

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