Theorem xrlelttrd 13086

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 13082	. . 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 5100  ℝ^*cxr 11177   < clt 11178   ≤ cle 11179

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 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379  ax-un 7690  ax-cnex 11094  ax-resscn 11095  ax-pre-lttri 11112  ax-pre-lttrn 11113

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 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-po 5540  df-so 5541  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-er 8645  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11180  df-mnf 11181  df-xr 11182  df-ltxr 11183  df-le 11184

This theorem is referenced by:  xlt2add  13187  ixxub  13294  elioc2  13337  elicc2  13339  limsupgre  15416  xrsdsreclblem  21379  mnfnei  23177  blgt0  24355  xblss2ps  24357  xblss2  24358  metustexhalf  24512  tgioo  24752  blcvx  24754  xrge0tsms  24791  metdcnlem  24793  metdscnlem  24812  ioombl  25534  uniioombllem1  25550  dvferm2lem  25958  dvlip2  25968  ftc1a  26012  coe1mul3  26072  ply1remlem  26138  idomrootle  26146  pserulm  26399  isblo3i  30888  xrge0infss  32850  iocinioc2  32869  xrge0tsmsd  33166  deg1addlt  33692  q1pvsca  33696  vietadeg1  33754  ply1degltdimlem  33799  ply1degltdim  33800  rtelextdg2lem  33903  sibfinima  34516  heicant  37903  itg2gt0cn  37923  ftc1anclem7  37947  ftc1anc  37949  dvrelog3  42432  aks6d1c5lem3  42504  aks6d1c6lem1  42537  aks6d1c6lem3  42539  supxrgelem  45693  supxrge  45694  xralrple2  45710  infxr  45722  infleinflem2  45726  xrralrecnnle  45738  unb2ltle  45770  eliocre  45866  iocopn  45877  ge0lere  45889  iccdificc  45896  limsupre  45996  limsuppnflem  46065  limsupre3lem  46087  limsupub2  46167  xlimmnfv  46189  fourierdlem27  46489  sge0isum  46782  meassre  46832  meaiuninclem  46835  omessre  46865  omeiunltfirp  46874  sge0hsphoire  46944  hoidmv1lelem1  46946  hoidmv1lelem2  46947  hoidmv1lelem3  46948  hoidmvlelem1  46950  hoidmvlelem4  46953  pimiooltgt  47065  pimincfltioc  47071  preimaleiinlt  47076  fsupdm  47197