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	⊢ 𝐴 ∈ Cℋ
	stle.2	⊢ 𝐵 ∈ Cℋ
	stm1add3.3	⊢ 𝐶 ∈ Cℋ
Assertion	stm1add3i	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) = 1 → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) + ( 𝑆 ‘ 𝐶 ) ) = 3 ) )

Proof

Step	Hyp	Ref	Expression
1		stle.1	⊢ 𝐴 ∈ Cℋ
2		stle.2	⊢ 𝐵 ∈ Cℋ
3		stm1add3.3	⊢ 𝐶 ∈ Cℋ
4	1 2	chincli	⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ
5	4 3	stm1i	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) = 1 → ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 ) )
6	1 2	stm1addi	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 ) )
7	5 6	syld	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) = 1 → ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 ) )
8	4 3	stm1ri	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) = 1 → ( 𝑆 ‘ 𝐶 ) = 1 ) )
9	7 8	jcad	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) = 1 → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 ∧ ( 𝑆 ‘ 𝐶 ) = 1 ) ) )
10		oveq12	⊢ ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 ∧ ( 𝑆 ‘ 𝐶 ) = 1 ) → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) + ( 𝑆 ‘ 𝐶 ) ) = ( 2 + 1 ) )
11		df-3	⊢ 3 = ( 2 + 1 )
12	10 11	eqtr4di	⊢ ( ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) = 2 ∧ ( 𝑆 ‘ 𝐶 ) = 1 ) → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) + ( 𝑆 ‘ 𝐶 ) ) = 3 )
13	9 12	syl6	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( ( 𝐴 ∩ 𝐵 ) ∩ 𝐶 ) ) = 1 → ( ( ( 𝑆 ‘ 𝐴 ) + ( 𝑆 ‘ 𝐵 ) ) + ( 𝑆 ‘ 𝐶 ) ) = 3 ) )