Metamath Proof Explorer


Theorem chcon2i

Description: Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses ch0le.1 AC
chjcl.2 BC
Assertion chcon2i A=BB=A

Proof

Step Hyp Ref Expression
1 ch0le.1 AC
2 chjcl.2 BC
3 1 2 chsscon2i ABBA
4 2 1 chsscon1i BAAB
5 3 4 anbi12i ABBABAAB
6 eqss A=BABBA
7 eqss B=ABAAB
8 5 6 7 3bitr4i A=BB=A