Metamath Proof Explorer


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 C
stle.2 B C
Assertion stm1ri S States S A B = 1 S B = 1

Proof

Step Hyp Ref Expression
1 stle.1 A C
2 stle.2 B C
3 incom A B = B A
4 3 fveq2i S A B = S B A
5 4 eqeq1i S A B = 1 S B A = 1
6 2 1 stm1i S States S B A = 1 S B = 1
7 5 6 syl5bi S States S A B = 1 S B = 1