Metamath Proof Explorer


Theorem stm1addi

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
Assertion stm1addi
|- ( S e. States -> ( ( S ` ( A i^i B ) ) = 1 -> ( ( S ` A ) + ( S ` B ) ) = 2 ) )

Proof

Step Hyp Ref Expression
1 stle.1
 |-  A e. CH
2 stle.2
 |-  B e. CH
3 1 2 stm1i
 |-  ( S e. States -> ( ( S ` ( A i^i B ) ) = 1 -> ( S ` A ) = 1 ) )
4 1 2 stm1ri
 |-  ( S e. States -> ( ( S ` ( A i^i B ) ) = 1 -> ( S ` B ) = 1 ) )
5 3 4 jcad
 |-  ( S e. States -> ( ( S ` ( A i^i B ) ) = 1 -> ( ( S ` A ) = 1 /\ ( S ` B ) = 1 ) ) )
6 oveq12
 |-  ( ( ( S ` A ) = 1 /\ ( S ` B ) = 1 ) -> ( ( S ` A ) + ( S ` B ) ) = ( 1 + 1 ) )
7 df-2
 |-  2 = ( 1 + 1 )
8 6 7 eqtr4di
 |-  ( ( ( S ` A ) = 1 /\ ( S ` B ) = 1 ) -> ( ( S ` A ) + ( S ` B ) ) = 2 )
9 5 8 syl6
 |-  ( S e. States -> ( ( S ` ( A i^i B ) ) = 1 -> ( ( S ` A ) + ( S ` B ) ) = 2 ) )