Theorem xrlelttrd 13156

Description: Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)

Hypotheses

Ref	Expression
xrlttrd.1	⊢ (𝜑 → 𝐴 ∈ ℝ*)
xrlttrd.2	⊢ (𝜑 → 𝐵 ∈ ℝ*)
xrlttrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ*)
xrlelttrd.4	⊢ (𝜑 → 𝐴 ≤ 𝐵)
xrlelttrd.5	⊢ (𝜑 → 𝐵 < 𝐶)

Assertion

Ref	Expression
xrlelttrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem xrlelttrd

Step	Hyp	Ref	Expression
1		xrlelttrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		xrlelttrd.5	. 2 ⊢ (𝜑 → 𝐵 < 𝐶)
3		xrlttrd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
4		xrlttrd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		xrlttrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ*)
6		xrlelttr 13152	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1389	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 709	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   class class class wbr 5097  ℝ^*cxr 11209   < clt 11210   ≤ cle 11211

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7713  ax-cnex 11123  ax-resscn 11124  ax-pre-lttri 11141  ax-pre-lttrn 11142

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-er 8672  df-en 8922  df-dom 8923  df-sdom 8924  df-pnf 11212  df-mnf 11213  df-xr 11214  df-ltxr 11215  df-le 11216

This theorem is referenced by:  xlt2add  13257  ixxub  13364  elioc2  13407  elicc2  13409  limsupgre  15499  xrsdsreclblem  21453  mnfnei  23269  blgt0  24447  xblss2ps  24449  xblss2  24450  metustexhalf  24604  tgioo  24844  blcvx  24846  xrge0tsms  24883  metdcnlem  24885  metdscnlem  24904  ioombl  25615  uniioombllem1  25631  dvferm2lem  26036  dvlip2  26045  ftc1a  26087  coe1mul3  26147  ply1remlem  26213  idomrootle  26221  pserulm  26473  isblo3i  30961  xrge0infss  32923  iocinioc2  32942  xrge0tsmsd  33214  deg1addlt  33757  q1pvsca  33761  vietadeg1  33836  ply1degltdimlem  33880  ply1degltdim  33881  rtelextdg2lem  33984  sibfinima  34597  heicant  38115  itg2gt0cn  38135  ftc1anclem7  38159  ftc1anc  38161  dvrelog3  42643  aks6d1c5lem3  42715  aks6d1c6lem1  42748  aks6d1c6lem3  42750  supxrgelem  45874  supxrge  45875  xralrple2  45891  infxr  45903  infleinflem2  45907  xrralrecnnle  45919  unb2ltle  45950  eliocre  46046  iocopn  46057  ge0lere  46069  iccdificc  46076  limsupre  46176  limsuppnflem  46245  limsupre3lem  46267  limsupub2  46347  xlimmnfv  46369  fourierdlem27  46669  sge0isum  46962  meassre  47012  meaiuninclem  47015  omessre  47045  omeiunltfirp  47054  sge0hsphoire  47124  hoidmv1lelem1  47126  hoidmv1lelem2  47127  hoidmv1lelem3  47128  hoidmvlelem1  47130  hoidmvlelem4  47133  pimiooltgt  47245  pimincfltioc  47251  preimaleiinlt  47256  fsupdm  47377