Metamath Proof Explorer

Theorem chsscon2

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

		Ref	Expression
	Assertion	chsscon2	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq ⊥ (B) \leftrightarrow B \subseteq ⊥ (A))$

Step	Hyp	Ref	Expression
1		chss	$⊢ A \in C_{ℋ} \to A \subseteq ℋ$
2		chss	$⊢ B \in C_{ℋ} \to B \subseteq ℋ$
3		occon3	$⊢ (A \subseteq ℋ \land B \subseteq ℋ) \to (A \subseteq ⊥ (B) \leftrightarrow B \subseteq ⊥ (A))$
4	1 2 3	syl2an	$⊢ (A \in C_{ℋ} \land B \in C_{ℋ}) \to (A \subseteq ⊥ (B) \leftrightarrow B \subseteq ⊥ (A))$