QLE Home Quantum Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  QLE Home  >  Th. List  >  gsth2 Unicode version
Theorem gsth2 490
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
StepHypRef Expression
1 gsth2.1 . . . . 5 b C c
21comcom 453 . . . 4 c C b
3 ancom 74 . . . . . . . . 9 (b ^ (b' v a')) = ((b' v a') ^ b)
4 ax-a2 31 . . . . . . . . . 10 (b' v a') = (a' v b')
54ran 78 . . . . . . . . 9 ((b' v a') ^ b) = ((a' v b') ^ b)
63, 5ax-r2 36 . . . . . . . 8 (b ^ (b' v a')) = ((a' v b') ^ b)
7 comor2 462 . . . . . . . . . 10 (a' v b') C b'
87comcom7 460 . . . . . . . . 9 (a' v b') C b
9 gsth2.2 . . . . . . . . . . . . 13 a C (b ^ c)
109comcom 453 . . . . . . . . . . . 12 (b ^ c) C a
1110comcom2 183 . . . . . . . . . . 11 (b ^ c) C a'
12 coman1 185 . . . . . . . . . . . 12 (b ^ c) C b
1312comcom2 183 . . . . . . . . . . 11 (b ^ c) C b'
1411, 13com2or 483 . . . . . . . . . 10 (b ^ c) C (a' v b')
1514comcom 453 . . . . . . . . 9 (a' v b') C (b ^ c)
168, 1, 15gsth 489 . . . . . . . 8 ((a' v b') ^ b) C c
176, 16bctr 181 . . . . . . 7 (b ^ (b' v a')) C c
1817comcom 453 . . . . . 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')'
2120lor 70 . . . . . . . . 9 (b' v (b ^ a)) = (b' v (b' v a')')
2221ax-r4 37 . . . . . . . 8 (b' v (b ^ a))' = (b' v (b' v a')')'
2322ax-r1 35 . . . . . . 7 (b' v (b' v a')')' = (b' v (b ^ a))'
2419, 23ax-r2 36 . . . . . 6 (b ^ (b' v a')) = (b' v (b ^ a))'
2518, 24cbtr 182 . . . . 5 c C (b' v (b ^ a))'
2625comcom7 460 . . . 4 c C (b' v (b ^ a))
272, 26com2an 484 . . 3 c C (b ^ (b' v (b ^ a)))
28 omla 447 . . . 4 (b ^ (b' v (b ^ a))) = (b ^ a)
29 ancom 74 . . . 4 (b ^ a) = (a ^ b)
3028, 29ax-r2 36 . . 3 (b ^ (b' v (b ^ a))) = (a ^ b)
3127, 30cbtr 182 . 2 c C (a ^ b)
3231comcom 453 1 (a ^ b) C c
Colors of variables: term
Syntax hints:   C wc 3  'wn 4   v wo 6   ^ wa 7
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
This theorem is referenced by:  gstho  491  oacom  1011  oacom3  1013
  Copyright terms: Public domain W3C validator