Theorem ltlecasei

Description: Ordering elimination by cases. (Contributed by NM, 1-Jul-2007) (Proof shortened by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypotheses	ltlecasei.1	$$⊢\left(\phi \wedge A<B\right)\to \psi$$
	ltlecasei.2	$$⊢\left(\phi \wedge B\le A\right)\to \psi$$
	ltlecasei.3	$$⊢\phi \to A\in ℝ$$
	ltlecasei.4	$$⊢\phi \to B\in ℝ$$
Assertion	ltlecasei	$$⊢\phi \to \psi$$

Proof

Step	Hyp	Ref	Expression
1		ltlecasei.1	$$⊢\left(\phi \wedge A<B\right)\to \psi$$
2		ltlecasei.2	$$⊢\left(\phi \wedge B\le A\right)\to \psi$$
3		ltlecasei.3	$$⊢\phi \to A\in ℝ$$
4		ltlecasei.4	$$⊢\phi \to B\in ℝ$$
5		lelttric	$$⊢\left(B\in ℝ\wedge A\in ℝ\right)\to \left(B\le A\vee A<B\right)$$
6	4 3 5	syl2anc	$$⊢\phi \to \left(B\le A\vee A<B\right)$$
7	2 1 6	mpjaodan	$$⊢\phi \to \psi$$