Theorem ltlecasei 11366

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 11365	. . 3 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 ≤ 𝐴 ∨ 𝐴 < 𝐵))
6	3, 4, 5	syl2anc 584	. 2 ⊢ (𝜑 → (𝐵 ≤ 𝐴 ∨ 𝐴 < 𝐵))
7	1, 2, 6	mpjaodan 960	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   ∈ wcel 2105   class class class wbr 5147  ℝcr 11151   < clt 11292   ≤ cle 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-xr 11296  df-le 11298

This theorem is referenced by:  iccsplit  13521  expnbnd  14267  hashf1  14492  absmax  15364  sinltx  16221  iccntr  24856  pmltpclem2  25497  cniccbdd  25509  iccvolcl  25615  ioovolcl  25618  dyaddisjlem  25643  mbfposr  25700  itg1ge0a  25760  itg2monolem1  25799  itgioo  25865  c1lip1  26050  plyeq0lem  26263  aalioulem5  26392  pserulm  26479  tanord  26594  birthdaylem3  27010  fsumharmonic  27069  chpo1ubb  27539  mblfinlem2  37644  metakunt9  42194  ioodvbdlimc1  45888  ioodvbdlimc2  45890  ibliooicc  45926  fourierdlem107  46168