Theorem xrletrd 13171

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

Hypotheses

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

Assertion

Ref	Expression
xrletrd	⊢ (𝜑 → 𝐴 ≤ 𝐶)

Proof of Theorem xrletrd

Step	Hyp	Ref	Expression
1		xrletrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		xrletrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		xrlttrd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
4		xrlttrd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		xrlttrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ*)
6		xrletr 13167	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
7	3, 4, 5, 6	syl3anc 1372	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 ≤ 𝐶))
8	1, 2, 7	mp2and 699	1 ⊢ (𝜑 → 𝐴 ≤ 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2107   class class class wbr 5117  ℝ^*cxr 11261   ≤ cle 11263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5264  ax-nul 5274  ax-pow 5333  ax-pr 5400  ax-un 7724  ax-cnex 11178  ax-resscn 11179  ax-pre-lttri 11196  ax-pre-lttrn 11197

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4882  df-br 5118  df-opab 5180  df-mpt 5200  df-id 5546  df-po 5559  df-so 5560  df-xp 5658  df-rel 5659  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665  df-iota 6481  df-fun 6530  df-fn 6531  df-f 6532  df-f1 6533  df-fo 6534  df-f1o 6535  df-fv 6536  df-er 8714  df-en 8955  df-dom 8956  df-sdom 8957  df-pnf 11264  df-mnf 11265  df-xr 11266  df-ltxr 11267  df-le 11268

This theorem is referenced by:  xaddge0  13267  ixxub  13375  ixxlb  13376  limsupval2  15485  0ram  17027  xpsdsval  24307  xblss2ps  24327  xblss2  24328  comet  24439  stdbdxmet  24441  nmoleub  24657  metnrmlem1  24786  nmoleub2lem  25052  ovollb2lem  25428  ovoliunlem2  25443  ovolscalem1  25453  ovolicc1  25456  ovolicc2lem4  25460  voliunlem2  25491  uniioombllem3  25525  itg2uba  25683  itg2lea  25684  itg2split  25689  itg2monolem3  25692  itg2gt0  25700  lhop1lem  25957  dvfsumlem2  25972  dvfsumlem2OLD  25973  dvfsumlem3  25974  dvfsumlem4  25975  deg1addle2  26046  deg1sublt  26054  nmooge0  30682  ply1degltlss  33541  metideq  33853  measiun  34178  omssubadd  34261  carsgclctunlem2  34280  mblfinlem1  37610  ismblfin  37614  ftc1anclem8  37653  ftc1anc  37654  aks6d1c6lem2  42113  aks6d1c6lem3  42114  unitscyglem5  42141  hbtlem2  43080  idomodle  43147  xle2addd  45297  xralrple2  45315  infleinflem1  45331  xralrple4  45334  xralrple3  45335  suplesup2  45337  infleinf2  45375  infxrlesupxr  45397  inficc  45497  limsupequzlem  45687  limsupvaluz2  45703  supcnvlimsup  45705  liminfval2  45733  liminflelimsuplem  45740  limsupgtlem  45742  fourierdlem1  46073  sge0cl  46346  sge0lefi  46363  sge0iunmptlemre  46380  sge0isum  46392  omeunle  46481  omeiunle  46482  caratheodorylem2  46492  hoicvrrex  46521  ovnsubaddlem1  46535  ovolval5lem1  46617  pimdecfgtioo  46682  pimincfltioo  46683