Metamath Proof Explorer


Theorem hstrbi

Description: Strong CH-state theorem (bidirectional version). Theorem in Mayet3 p. 10 and its converse. (Contributed by NM, 30-Jun-2006) (New usage is discouraged.)

Ref Expression
Hypotheses hstr.1 A C
hstr.2 B C
Assertion hstrbi f CHStates norm f A = 1 norm f B = 1 A B

Proof

Step Hyp Ref Expression
1 hstr.1 A C
2 hstr.2 B C
3 1 2 hstri f CHStates norm f A = 1 norm f B = 1 A B
4 hstles f CHStates A C B C A B norm f A = 1 norm f B = 1
5 2 4 mpanr1 f CHStates A C A B norm f A = 1 norm f B = 1
6 1 5 mpanl2 f CHStates A B norm f A = 1 norm f B = 1
7 6 expcom A B f CHStates norm f A = 1 norm f B = 1
8 7 ralrimiv A B f CHStates norm f A = 1 norm f B = 1
9 3 8 impbii f CHStates norm f A = 1 norm f B = 1 A B