Metamath Proof Explorer


Theorem stcltr2i

Description: Property of a strong classical state. (Contributed by NM, 24-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses stcltr1.1 φSStatesxCyCSx=1Sy=1xy
stcltr1.2 AC
Assertion stcltr2i φSA=1A=

Proof

Step Hyp Ref Expression
1 stcltr1.1 φSStatesxCyCSx=1Sy=1xy
2 stcltr1.2 AC
3 ax-1 SA=1S=1SA=1
4 helch C
5 1 4 2 stcltr1i φS=1SA=1A
6 3 5 syl5 φSA=1A
7 2 chssii A
8 eqss A=AA
9 7 8 mpbiran A=A
10 6 9 syl6ibr φSA=1A=