This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cvnref

Description: The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004) (New usage is discouraged.)

		Ref	Expression
	Assertion	cvnref	$⊢ A \in C_{ℋ} \to \neg A ⋖_{ℋ} A$

Step	Hyp	Ref	Expression
1		cvnsym	$⊢ (A \in C_{ℋ} \land A \in C_{ℋ}) \to (A ⋖_{ℋ} A \to \neg A ⋖_{ℋ} A)$
2	1	anidms	$⊢ A \in C_{ℋ} \to (A ⋖_{ℋ} A \to \neg A ⋖_{ℋ} A)$
3	2	pm2.01d	$⊢ A \in C_{ℋ} \to \neg A ⋖_{ℋ} A$