Theorem stm1ri

Description: State of component of unit meet. (Contributed by NM, 11-Nov-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	stle.1	⊢ 𝐴 ∈ Cℋ
	stle.2	⊢ 𝐵 ∈ Cℋ
Assertion	stm1ri	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) )

Proof

Step	Hyp	Ref	Expression
1		stle.1	⊢ 𝐴 ∈ Cℋ
2		stle.2	⊢ 𝐵 ∈ Cℋ
3		incom	⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
4	3	fveq2i	⊢ ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑆 ‘ ( 𝐵 ∩ 𝐴 ) )
5	4	eqeq1i	⊢ ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 ↔ ( 𝑆 ‘ ( 𝐵 ∩ 𝐴 ) ) = 1 )
6	2 1	stm1i	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐵 ∩ 𝐴 ) ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) )
7	5 6	biimtrid	⊢ ( 𝑆 ∈ States → ( ( 𝑆 ‘ ( 𝐴 ∩ 𝐵 ) ) = 1 → ( 𝑆 ‘ 𝐵 ) = 1 ) )