Theorem lttri5d

Description: Not equal and not larger implies smaller. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	lttri5d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	lttri5d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	lttri5d.aneb	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
	lttri5d.nlt	⊢ ( 𝜑 → ¬ 𝐵 < 𝐴 )
Assertion	lttri5d	⊢ ( 𝜑 → 𝐴 < 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		lttri5d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		lttri5d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		lttri5d.aneb	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
4		lttri5d.nlt	⊢ ( 𝜑 → ¬ 𝐵 < 𝐴 )
5	1	rexrd	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
6	2	rexrd	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
7	5 6 3 4	xrlttri5d	⊢ ( 𝜑 → 𝐴 < 𝐵 )