Metamath Proof Explorer


Theorem chsscon2i

Description: Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 AC
chjcl.2 BC
Assertion chsscon2i ABBA

Proof

Step Hyp Ref Expression
1 ch0le.1 AC
2 chjcl.2 BC
3 1 chssii A
4 2 chssii B
5 occon3 ABABBA
6 3 4 5 mp2an ABBA