Metamath Proof Explorer


Theorem stm1add3i

Description: Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

Ref Expression
Hypotheses stle.1 A C
stle.2 B C
stm1add3.3 C C
Assertion stm1add3i S States S A B C = 1 S A + S B + S C = 3

Proof

Step Hyp Ref Expression
1 stle.1 A C
2 stle.2 B C
3 stm1add3.3 C C
4 1 2 chincli A B C
5 4 3 stm1i S States S A B C = 1 S A B = 1
6 1 2 stm1addi S States S A B = 1 S A + S B = 2
7 5 6 syld S States S A B C = 1 S A + S B = 2
8 4 3 stm1ri S States S A B C = 1 S C = 1
9 7 8 jcad S States S A B C = 1 S A + S B = 2 S C = 1
10 oveq12 S A + S B = 2 S C = 1 S A + S B + S C = 2 + 1
11 df-3 3 = 2 + 1
12 10 11 eqtr4di S A + S B = 2 S C = 1 S A + S B + S C = 3
13 9 12 syl6 S States S A B C = 1 S A + S B + S C = 3