Theorem ltlecasei 11253

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   ∈ wcel 2114   class class class wbr 5100  ℝcr 11037   < clt 11178   ≤ cle 11179

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-xr 11182  df-le 11184

This theorem is referenced by:  iccsplit  13413  expnbnd  14167  hashf1  14392  absmax  15265  sinltx  16126  iccntr  24778  pmltpclem2  25418  cniccbdd  25430  iccvolcl  25536  ioovolcl  25539  dyaddisjlem  25564  mbfposr  25621  itg1ge0a  25680  itg2monolem1  25719  itgioo  25785  c1lip1  25970  plyeq0lem  26183  aalioulem5  26312  pserulm  26399  tanord  26515  birthdaylem3  26931  fsumharmonic  26990  chpo1ubb  27460  cos9thpiminplylem1  33959  mblfinlem2  37906  ioodvbdlimc1  46288  ioodvbdlimc2  46290  ibliooicc  46326  fourierdlem107  46568