Theorem stm1ri

Description: State of component of unit meet. (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}}$$
Assertion	stm1ri	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(B\right)=1\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		incom	$$⊢A\cap B=B\cap A$$
4	3	fveq2i	$$⊢S\left(A\cap B\right)=S\left(B\cap A\right)$$
5	4	eqeq1i	$$⊢S\left(A\cap B\right)=1\leftrightarrow S\left(B\cap A\right)=1$$
6	2 1	stm1i	$$⊢S\in \mathrm{States}\to \left(S\left(B\cap A\right)=1\to S\left(B\right)=1\right)$$
7	5 6	biimtrid	$$⊢S\in \mathrm{States}\to \left(S\left(A\cap B\right)=1\to S\left(B\right)=1\right)$$