Theorem ltlecasei 11411

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

Hypotheses

Ref	Expression
ltlecasei.1	⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝜓)
ltlecasei.2	⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓)
ltlecasei.3	⊢ (𝜑 → 𝐴 ∈ ℝ)
ltlecasei.4	⊢ (𝜑 → 𝐵 ∈ ℝ)

Assertion

Ref	Expression
ltlecasei	⊢ (𝜑 → 𝜓)

Proof of Theorem ltlecasei

Step	Hyp	Ref	Expression
1		ltlecasei.2	. 2 ⊢ ((𝜑 ∧ 𝐵 ≤ 𝐴) → 𝜓)
2		ltlecasei.1	. 2 ⊢ ((𝜑 ∧ 𝐴 < 𝐵) → 𝜓)
3		ltlecasei.4	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
4		ltlecasei.3	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
5		lelttric 11410	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ∨ 𝐴 < 𝐵))
6	3, 4, 5	syl2anc 596	. 2 ⊢ (𝜑 → (𝐵 ≤ 𝐴 ∨ 𝐴 < 𝐵))
7	1, 2, 6	mpjaodan 973	1 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∈ wcel 2145   class class class wbr 5103  ℝcr 11192   < clt 11336   ≤ cle 11337

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-xr 11340  df-le 11342

This theorem is used by:  iccsplit  13609  expnbnd  14369  hashf1  14595  absmax  15490  sinltx  16350  iccntr  25134  pmltpclem2  25763  cniccbdd  25775  iccvolcl  25881  ioovolcl  25884  dyaddisjlem  25909  mbfposr  25966  itg1ge0a  26025  itg2monolem1  26064  itgioo  26129  c1lip1  26310  plyeq0lem  26522  aalioulem5  26656  pserulm  26742  tanord  26859  birthdaylem3  27274  fsumharmonic  27332  chpo1ubb  27801  cos9thpiminplylem1  34407  mblfinlem2  38556  ioodvbdlimc1  46912  ioodvbdlimc2  46914  ibliooicc  46950  fourierdlem107  47192