Theorem chsscon2i

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

	Ref	Expression
Hypotheses	ch0le.1	|- A e. CH
	chjcl.2	|- B e. CH
Assertion	chsscon2i	|- ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) )

Proof

Step	Hyp	Ref	Expression
1		ch0le.1	|- A e. CH
2		chjcl.2	|- B e. CH
3	1	chssii	|- A C_ ~H
4	2	chssii	|- B C_ ~H
5		occon3	|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) ) )
6	3 4 5	mp2an	|- ( A C_ ( _|_ ` B ) <-> B C_ ( _|_ ` A ) )