Theorem xrletrd 13140

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

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   class class class wbr 5148  ℝ^*cxr 11246   ≤ cle 11248

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-cnex 11165  ax-resscn 11166  ax-pre-lttri 11183  ax-pre-lttrn 11184

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-po 5588  df-so 5589  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-er 8702  df-en 8939  df-dom 8940  df-sdom 8941  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253

This theorem is referenced by:  xaddge0  13236  ixxub  13344  ixxlb  13345  limsupval2  15423  0ram  16952  xpsdsval  23886  xblss2ps  23906  xblss2  23907  comet  24021  stdbdxmet  24023  nmoleub  24247  metnrmlem1  24374  nmoleub2lem  24629  ovollb2lem  25004  ovoliunlem2  25019  ovolscalem1  25029  ovolicc1  25032  ovolicc2lem4  25036  voliunlem2  25067  uniioombllem3  25101  itg2uba  25260  itg2lea  25261  itg2split  25266  itg2monolem3  25269  itg2gt0  25277  lhop1lem  25529  dvfsumlem2  25543  dvfsumlem3  25544  dvfsumlem4  25545  deg1addle2  25619  deg1sublt  25627  nmooge0  30015  ply1degltlss  32662  metideq  32868  measiun  33211  omssubadd  33294  carsgclctunlem2  33313  gg-dvfsumlem2  35178  mblfinlem1  36520  ismblfin  36524  ftc1anclem8  36563  ftc1anc  36564  hbtlem2  41856  idomodle  41928  xle2addd  44036  xralrple2  44054  infleinflem1  44070  xralrple4  44073  xralrple3  44074  suplesup2  44076  infleinf2  44114  infxrlesupxr  44136  inficc  44237  limsupequzlem  44428  limsupvaluz2  44444  supcnvlimsup  44446  liminfval2  44474  liminflelimsuplem  44481  limsupgtlem  44483  fourierdlem1  44814  sge0cl  45087  sge0lefi  45104  sge0iunmptlemre  45121  sge0isum  45133  omeunle  45222  omeiunle  45223  caratheodorylem2  45233  hoicvrrex  45262  ovnsubaddlem1  45276  ovolval5lem1  45358  pimdecfgtioo  45423  pimincfltioo  45424