Theorem xrlelttrd 13075

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 13071	. . 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 11166   < clt 11167   ≤ cle 11168

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 5300  ax-pr 5368  ax-un 7680  ax-cnex 11083  ax-resscn 11084  ax-pre-lttri 11101  ax-pre-lttrn 11102

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 5517  df-po 5530  df-so 5531  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-er 8634  df-en 8885  df-dom 8886  df-sdom 8887  df-pnf 11169  df-mnf 11170  df-xr 11171  df-ltxr 11172  df-le 11173

This theorem is referenced by:  xlt2add  13176  ixxub  13283  elioc2  13326  elicc2  13328  limsupgre  15405  xrsdsreclblem  21369  mnfnei  23164  blgt0  24342  xblss2ps  24344  xblss2  24345  metustexhalf  24499  tgioo  24739  blcvx  24741  xrge0tsms  24778  metdcnlem  24780  metdscnlem  24799  ioombl  25510  uniioombllem1  25526  dvferm2lem  25931  dvlip2  25941  ftc1a  25985  coe1mul3  26045  ply1remlem  26111  idomrootle  26119  pserulm  26371  isblo3i  30861  xrge0infss  32823  iocinioc2  32842  xrge0tsmsd  33139  deg1addlt  33665  q1pvsca  33669  vietadeg1  33727  ply1degltdimlem  33772  ply1degltdim  33773  rtelextdg2lem  33876  sibfinima  34489  heicant  37967  itg2gt0cn  37987  ftc1anclem7  38011  ftc1anc  38013  dvrelog3  42496  aks6d1c5lem3  42568  aks6d1c6lem1  42601  aks6d1c6lem3  42603  supxrgelem  45770  supxrge  45771  xralrple2  45787  infxr  45799  infleinflem2  45803  xrralrecnnle  45815  unb2ltle  45847  eliocre  45943  iocopn  45954  ge0lere  45966  iccdificc  45973  limsupre  46073  limsuppnflem  46142  limsupre3lem  46164  limsupub2  46244  xlimmnfv  46266  fourierdlem27  46566  sge0isum  46859  meassre  46909  meaiuninclem  46912  omessre  46942  omeiunltfirp  46951  sge0hsphoire  47021  hoidmv1lelem1  47023  hoidmv1lelem2  47024  hoidmv1lelem3  47025  hoidmvlelem1  47027  hoidmvlelem4  47030  pimiooltgt  47142  pimincfltioc  47148  preimaleiinlt  47153  fsupdm  47274