Theorem occon2i

Description: Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000) (New usage is discouraged.)

	Ref	Expression
Hypotheses	occon2.1	|- A C_ ~H
	occon2.2	|- B C_ ~H
Assertion	occon2i	|- ( A C_ B -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		occon2.1	|- A C_ ~H
2		occon2.2	|- B C_ ~H
3		occon2	|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A C_ B -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` B ) ) ) )
4	1 2 3	mp2an	|- ( A C_ B -> ( _|_ ` ( _|_ ` A ) ) C_ ( _|_ ` ( _|_ ` B ) ) )