Theorem xrlelttrd 13198

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   class class class wbr 5147  ℝ^*cxr 11291   < clt 11292   ≤ cle 11293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-pre-lttri 11226  ax-pre-lttrn 11227

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-po 5596  df-so 5597  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-er 8743  df-en 8984  df-dom 8985  df-sdom 8986  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298

This theorem is referenced by:  xlt2add  13298  ixxub  13404  elioc2  13446  elicc2  13448  limsupgre  15513  xrsdsreclblem  21447  mnfnei  23244  blgt0  24424  xblss2ps  24426  xblss2  24427  metustexhalf  24584  tgioo  24831  blcvx  24833  xrge0tsms  24869  metdcnlem  24871  metdscnlem  24890  ioombl  25613  uniioombllem1  25629  dvferm2lem  26038  dvlip2  26048  ftc1a  26092  coe1mul3  26152  ply1remlem  26218  idomrootle  26226  pserulm  26479  isblo3i  30829  xrge0infss  32770  iocinioc2  32787  xrge0tsmsd  33047  deg1addlt  33599  q1pvsca  33603  ply1degltdimlem  33649  ply1degltdim  33650  rtelextdg2lem  33731  sibfinima  34320  heicant  37641  itg2gt0cn  37661  ftc1anclem7  37685  ftc1anc  37687  dvrelog3  42046  aks6d1c5lem3  42118  aks6d1c6lem1  42151  aks6d1c6lem3  42153  supxrgelem  45286  supxrge  45287  xralrple2  45303  infxr  45316  infleinflem2  45320  xrralrecnnle  45332  unb2ltle  45364  eliocre  45461  iocopn  45472  ge0lere  45484  iccdificc  45491  limsupre  45596  limsuppnflem  45665  limsupre3lem  45687  limsupub2  45767  xlimmnfv  45789  fourierdlem27  46089  sge0isum  46382  meassre  46432  meaiuninclem  46435  omessre  46465  omeiunltfirp  46474  sge0hsphoire  46544  hoidmv1lelem1  46546  hoidmv1lelem2  46547  hoidmv1lelem3  46548  hoidmvlelem1  46550  hoidmvlelem4  46553  pimiooltgt  46665  pimincfltioc  46671  preimaleiinlt  46676  fsupdm  46797