Theorem xrlelttrd 13102

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 13098	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1374	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 700	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   class class class wbr 5086  ℝ^*cxr 11169   < clt 11170   ≤ cle 11171

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-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682  ax-cnex 11085  ax-resscn 11086  ax-pre-lttri 11103  ax-pre-lttrn 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-nel 3038  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-po 5532  df-so 5533  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-er 8636  df-en 8887  df-dom 8888  df-sdom 8889  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176

This theorem is referenced by:  xlt2add  13203  ixxub  13310  elioc2  13353  elicc2  13355  limsupgre  15434  xrsdsreclblem  21402  mnfnei  23196  blgt0  24374  xblss2ps  24376  xblss2  24377  metustexhalf  24531  tgioo  24771  blcvx  24773  xrge0tsms  24810  metdcnlem  24812  metdscnlem  24831  ioombl  25542  uniioombllem1  25558  dvferm2lem  25963  dvlip2  25972  ftc1a  26014  coe1mul3  26074  ply1remlem  26140  idomrootle  26148  pserulm  26400  isblo3i  30887  xrge0infss  32848  iocinioc2  32867  xrge0tsmsd  33149  deg1addlt  33675  q1pvsca  33679  vietadeg1  33737  ply1degltdimlem  33782  ply1degltdim  33783  rtelextdg2lem  33886  sibfinima  34499  heicant  37990  itg2gt0cn  38010  ftc1anclem7  38034  ftc1anc  38036  dvrelog3  42518  aks6d1c5lem3  42590  aks6d1c6lem1  42623  aks6d1c6lem3  42625  supxrgelem  45785  supxrge  45786  xralrple2  45802  infxr  45814  infleinflem2  45818  xrralrecnnle  45830  unb2ltle  45861  eliocre  45957  iocopn  45968  ge0lere  45980  iccdificc  45987  limsupre  46087  limsuppnflem  46156  limsupre3lem  46178  limsupub2  46258  xlimmnfv  46280  fourierdlem27  46580  sge0isum  46873  meassre  46923  meaiuninclem  46926  omessre  46956  omeiunltfirp  46965  sge0hsphoire  47035  hoidmv1lelem1  47037  hoidmv1lelem2  47038  hoidmv1lelem3  47039  hoidmvlelem1  47041  hoidmvlelem4  47044  pimiooltgt  47156  pimincfltioc  47162  preimaleiinlt  47167  fsupdm  47288