Theorem xrlttri5d

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

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

Proof

Step	Hyp	Ref	Expression
1		xrlttri5d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2		xrlttri5d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3		xrlttri5d.aneb	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
4		xrlttri5d.nlt	⊢ ( 𝜑 → ¬ 𝐵 < 𝐴 )
5	3	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = 𝐵 )
6		xrlttri3	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 = 𝐵 ↔ ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) ) )
7	1 2 6	syl2anc	⊢ ( 𝜑 → ( 𝐴 = 𝐵 ↔ ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) ) )
8	5 7	mtbid	⊢ ( 𝜑 → ¬ ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) )
9		oran	⊢ ( ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ↔ ¬ ( ¬ 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) )
10	8 9	sylibr	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) )
11	10 4	jca	⊢ ( 𝜑 → ( ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ∧ ¬ 𝐵 < 𝐴 ) )
12		pm5.61	⊢ ( ( ( 𝐴 < 𝐵 ∨ 𝐵 < 𝐴 ) ∧ ¬ 𝐵 < 𝐴 ) ↔ ( 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) )
13	11 12	sylib	⊢ ( 𝜑 → ( 𝐴 < 𝐵 ∧ ¬ 𝐵 < 𝐴 ) )
14	13	simpld	⊢ ( 𝜑 → 𝐴 < 𝐵 )