MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ltlecasei Structured version   Visualization version   GIF version

Theorem ltlecasei 10819
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
StepHypRef Expression
1 ltlecasei.2 . 2 ((𝜑𝐵𝐴) → 𝜓)
2 ltlecasei.1 . 2 ((𝜑𝐴 < 𝐵) → 𝜓)
3 ltlecasei.4 . . 3 (𝜑𝐵 ∈ ℝ)
4 ltlecasei.3 . . 3 (𝜑𝐴 ∈ ℝ)
5 lelttric 10818 . . 3 ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵𝐴𝐴 < 𝐵))
63, 4, 5syl2anc 587 . 2 (𝜑 → (𝐵𝐴𝐴 < 𝐵))
71, 2, 6mpjaodan 958 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wo 846  wcel 2113   class class class wbr 5027  cr 10607   < clt 10746  cle 10747
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-ral 3058  df-rex 3059  df-v 3399  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-br 5028  df-opab 5090  df-xp 5525  df-cnv 5527  df-xr 10750  df-le 10752
This theorem is referenced by:  iccsplit  12952  expnbnd  13678  hashf1  13902  absmax  14772  sinltx  15627  iccntr  23566  pmltpclem2  24194  cniccbdd  24206  iccvolcl  24312  ioovolcl  24315  dyaddisjlem  24340  mbfposr  24397  itg1ge0a  24456  itg2monolem1  24495  itgioo  24560  c1lip1  24741  plyeq0lem  24951  aalioulem5  25076  pserulm  25161  tanord  25274  birthdaylem3  25683  fsumharmonic  25741  chpo1ubb  26209  mblfinlem2  35427  metakunt9  39713  ioodvbdlimc1  43000  ioodvbdlimc2  43002  ibliooicc  43038  fourierdlem107  43280
  Copyright terms: Public domain W3C validator