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

Metamath Proof Explorer

Theorem leid

Description: 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999)

		Ref	Expression
	Assertion	leid	$⊢ A \in ℝ \to A \leq A$

Step	Hyp	Ref	Expression
1		eqid	$⊢ A = A$
2	1	olci	$⊢ (A < A \lor A = A)$
3		leloe	$⊢ (A \in ℝ \land A \in ℝ) \to (A \leq A \leftrightarrow (A < A \lor A = A))$
4	2 3	mpbiri	$⊢ (A \in ℝ \land A \in ℝ) \to A \leq A$
5	4	anidms	$⊢ A \in ℝ \to A \leq A$