Theorem ltlecasei 10740

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

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   ∈ wcel 2108   class class class wbr 5057  ℝcr 10528   < clt 10667   ≤ cle 10668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pr 5320

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1084  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ral 3141  df-rex 3142  df-rab 3145  df-v 3495  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-nul 4290  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5058  df-opab 5120  df-xp 5554  df-cnv 5556  df-xr 10671  df-le 10673

This theorem is referenced by:  iccsplit  12863  expnbnd  13585  hashf1  13807  absmax  14681  sinltx  15534  iccntr  23421  pmltpclem2  24042  cniccbdd  24054  iccvolcl  24160  ioovolcl  24163  dyaddisjlem  24188  mbfposr  24245  itg1ge0a  24304  itg2monolem1  24343  itgioo  24408  c1lip1  24586  plyeq0lem  24792  aalioulem5  24917  pserulm  25002  tanord  25114  birthdaylem3  25523  fsumharmonic  25581  chpo1ubb  26049  mblfinlem2  34922  ioodvbdlimc1  42207  ioodvbdlimc2  42209  ibliooicc  42245  fourierdlem107  42488