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\in {\mathbf{C}}_{\mathscr{H}}$$
	stle.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
	stm1add3.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
Assertion	stm1add3i	$$⊢S\in \mathrm{States}\to \left(S\left(\left(A\cap B\right)\cap C\right)=1\to S\left(A\right)+S\left(B\right)+S\left(C\right)=3\right)$$

Proof

Step	Hyp	Ref	Expression
1		stle.1	$$⊢A\in {\mathbf{C}}_{\mathscr{H}}$$
2		stle.2	$$⊢B\in {\mathbf{C}}_{\mathscr{H}}$$
3		stm1add3.3	$$⊢C\in {\mathbf{C}}_{\mathscr{H}}$$
4	1 2	chincli	$$⊢A\cap B\in {\mathbf{C}}_{\mathscr{H}}$$
5	4 3	stm1i	$$⊢S\in \mathrm{States}\to \left(S\left(\left(A\cap B\right)\cap C\right)=1\to S\left(A\cap B\right)=1\right)$$
6	1 2	stm1addi	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(A\right)+S\left(B\right)=2\right)$$
7	5 6	syld	$$⊢S\in \mathrm{States}\to \left(S\left(\left(A\cap B\right)\cap C\right)=1\to S\left(A\right)+S\left(B\right)=2\right)$$
8	4 3	stm1ri	$$⊢S\in \mathrm{States}\to \left(S\left(\left(A\cap B\right)\cap C\right)=1\to S\left(C\right)=1\right)$$
9	7 8	jcad	$$⊢S\in \mathrm{States}\to \left(S\left(\left(A\cap B\right)\cap C\right)=1\to \left(S\left(A\right)+S\left(B\right)=2\wedge S\left(C\right)=1\right)\right)$$
10		oveq12	$$⊢\left(S\left(A\right)+S\left(B\right)=2\wedge S\left(C\right)=1\right)\to S\left(A\right)+S\left(B\right)+S\left(C\right)=2+1$$
11		df-3	$$⊢3=2+1$$
12	10 11	eqtr4di	$$⊢\left(S\left(A\right)+S\left(B\right)=2\wedge S\left(C\right)=1\right)\to S\left(A\right)+S\left(B\right)+S\left(C\right)=3$$
13	9 12	syl6	$$⊢S\in \mathrm{States}\to \left(S\left(\left(A\cap B\right)\cap C\right)=1\to S\left(A\right)+S\left(B\right)+S\left(C\right)=3\right)$$