Theorem xrletrd 13157

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   class class class wbr 5097  ℝ^*cxr 11208   ≤ cle 11210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pow 5319  ax-pr 5387  ax-un 7712  ax-cnex 11122  ax-resscn 11123  ax-pre-lttri 11140  ax-pre-lttrn 11141

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1098  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-nel 3061  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-po 5551  df-so 5552  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6471  df-fun 6517  df-fn 6518  df-f 6519  df-f1 6520  df-fo 6521  df-f1o 6522  df-fv 6523  df-er 8671  df-en 8921  df-dom 8922  df-sdom 8923  df-pnf 11211  df-mnf 11212  df-xr 11213  df-ltxr 11214  df-le 11215

This theorem is referenced by:  xaddge0  13254  ixxub  13363  ixxlb  13364  limsupval2  15497  0ram  17046  xpsdsval  24428  xblss2ps  24448  xblss2  24449  comet  24560  stdbdxmet  24562  nmoleub  24778  metnrmlem1  24907  nmoleub2lem  25163  ovollb2lem  25537  ovoliunlem2  25552  ovolscalem1  25562  ovolicc1  25565  ovolicc2lem4  25569  voliunlem2  25600  uniioombllem3  25634  itg2uba  25792  itg2lea  25793  itg2split  25798  itg2monolem3  25801  itg2gt0  25809  lhop1lem  26062  dvfsumlem2  26076  dvfsumlem3  26077  dvfsumlem4  26078  deg1addle2  26149  deg1sublt  26157  nmooge0  30926  ply1degltlss  33752  metideq  34150  measiun  34475  omssubadd  34557  carsgclctunlem2  34576  mblfinlem1  38116  ismblfin  38120  ftc1anclem8  38159  ftc1anc  38160  aks6d1c6lem2  42748  aks6d1c6lem3  42749  unitscyglem5  42776  hbtlem2  43661  idomodle  43728  xle2addd  45872  xralrple2  45890  infleinflem1  45905  xralrple4  45908  xralrple3  45909  suplesup2  45911  infleinf2  45948  infxrlesupxr  45970  inficc  46070  limsupequzlem  46256  limsupvaluz2  46272  supcnvlimsup  46274  liminfval2  46302  liminflelimsuplem  46309  limsupgtlem  46311  fourierdlem1  46642  sge0cl  46915  sge0lefi  46932  sge0iunmptlemre  46949  sge0isum  46961  omeunle  47050  omeiunle  47051  caratheodorylem2  47061  hoicvrrex  47090  ovnsubaddlem1  47104  ovolval5lem1  47186  pimdecfgtioo  47251  pimincfltioo  47252