Theorem xrletrd 13188

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   class class class wbr 5110  ℝ^*cxr 11243   ≤ cle 11245

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5258  ax-nul 5270  ax-pow 5338  ax-pr 5406  ax-un 7734  ax-cnex 11157  ax-resscn 11158  ax-pre-lttri 11175  ax-pre-lttrn 11176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3746  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-pw 4565  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5558  df-po 5571  df-so 5572  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-er 8695  df-en 8945  df-dom 8946  df-sdom 8947  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250

This theorem is referenced by:  xaddge0  13285  ixxub  13394  ixxlb  13395  limsupval2  15533  0ram  17081  xpsdsval  24519  xblss2ps  24539  xblss2  24540  comet  24651  stdbdxmet  24653  nmoleub  24869  metnrmlem1  24998  nmoleub2lem  25254  ovollb2lem  25628  ovoliunlem2  25643  ovolscalem1  25653  ovolicc1  25656  ovolicc2lem4  25660  voliunlem2  25691  uniioombllem3  25725  itg2uba  25883  itg2lea  25884  itg2split  25889  itg2monolem3  25892  itg2gt0  25900  lhop1lem  26153  dvfsumlem2  26167  dvfsumlem3  26168  dvfsumlem4  26169  deg1addle2  26240  deg1sublt  26248  nmooge0  31100  ply1degltlss  33867  metideq  34264  measiun  34589  omssubadd  34671  carsgclctunlem2  34690  mblfinlem1  38289  ismblfin  38293  ftc1anclem8  38332  ftc1anc  38333  aks6d1c6lem2  42919  aks6d1c6lem3  42920  unitscyglem5  42947  hbtlem2  43834  idomodle  43901  xle2addd  46035  xralrple2  46053  infleinflem1  46068  xralrple4  46071  xralrple3  46072  suplesup2  46074  infleinf2  46111  infxrlesupxr  46133  inficc  46233  limsupequzlem  46419  limsupvaluz2  46435  supcnvlimsup  46437  liminfval2  46465  liminflelimsuplem  46472  limsupgtlem  46474  fourierdlem1  46805  sge0cl  47078  sge0lefi  47095  sge0iunmptlemre  47112  sge0isum  47124  omeunle  47213  omeiunle  47214  caratheodorylem2  47224  hoicvrrex  47253  ovnsubaddlem1  47267  ovolval5lem1  47349  pimdecfgtioo  47414  pimincfltioo  47415