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

Metamath Proof Explorer

Theorem ltle

Description: 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999)

Ref Expression
Assertion ltle ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → A ≤ B

Proof

Step Hyp Ref Expression
1 orc ⊢ A < B → A < B ∨ A = B
2 leloe ⊢ A ∈ ℝ ∧ B ∈ ℝ → A ≤ B ↔ A < B ∨ A = B
3 1 2 imbitrrid ⊢ A ∈ ℝ ∧ B ∈ ℝ → A < B → A ≤ B