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 ) ) |