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 e. CH
stle.2 
|- B e. CH
stm1add3.3 
|- C e. CH
Assertion stm1add3i 
|- ( S e. States -> ( ( S ` ( ( A i^i B ) i^i C ) ) = 1 -> ( ( ( S ` A ) + ( S ` B ) ) + ( S ` C ) ) = 3 ) )

Proof

Step Hyp Ref Expression
1 stle.1 
 |-  A e. CH
2 stle.2 
 |-  B e. CH
3 stm1add3.3 
 |-  C e. CH
4 1 2 chincli 
 |-  ( A i^i B ) e. CH
5 4 3 stm1i 
 |-  ( S e. States -> ( ( S ` ( ( A i^i B ) i^i C ) ) = 1 -> ( S ` ( A i^i B ) ) = 1 ) )
6 1 2 stm1addi 
 |-  ( S e. States -> ( ( S ` ( A i^i B ) ) = 1 -> ( ( S ` A ) + ( S ` B ) ) = 2 ) )
7 5 6 syld 
 |-  ( S e. States -> ( ( S ` ( ( A i^i B ) i^i C ) ) = 1 -> ( ( S ` A ) + ( S ` B ) ) = 2 ) )
8 4 3 stm1ri 
 |-  ( S e. States -> ( ( S ` ( ( A i^i B ) i^i C ) ) = 1 -> ( S ` C ) = 1 ) )
9 7 8 jcad 
 |-  ( S e. States -> ( ( S ` ( ( A i^i B ) i^i 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 e. States -> ( ( S ` ( ( A i^i B ) i^i C ) ) = 1 -> ( ( ( S ` A ) + ( S ` B ) ) + ( S ` C ) ) = 3 ) )