Theorem xrletrd 13150

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2132   class class class wbr 5090  ℝ^*cxr 11201   ≤ cle 11203

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pow 5312  ax-pr 5380  ax-un 7703  ax-cnex 11115  ax-resscn 11116  ax-pre-lttri 11133  ax-pre-lttrn 11134

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3or 1096  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-nel 3052  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-pw 4547  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-po 5544  df-so 5545  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fn 6509  df-f 6510  df-f1 6511  df-fo 6512  df-f1o 6513  df-fv 6514  df-er 8662  df-en 8913  df-dom 8914  df-sdom 8915  df-pnf 11204  df-mnf 11205  df-xr 11206  df-ltxr 11207  df-le 11208

This theorem is referenced by:  xaddge0  13247  ixxub  13356  ixxlb  13357  limsupval2  15479  0ram  17028  xpsdsval  24410  xblss2ps  24430  xblss2  24431  comet  24542  stdbdxmet  24544  nmoleub  24760  metnrmlem1  24889  nmoleub2lem  25145  ovollb2lem  25519  ovoliunlem2  25534  ovolscalem1  25544  ovolicc1  25547  ovolicc2lem4  25551  voliunlem2  25582  uniioombllem3  25616  itg2uba  25774  itg2lea  25775  itg2split  25780  itg2monolem3  25783  itg2gt0  25791  lhop1lem  26044  dvfsumlem2  26058  dvfsumlem3  26059  dvfsumlem4  26060  deg1addle2  26131  deg1sublt  26139  nmooge0  30905  ply1degltlss  33736  metideq  34134  measiun  34459  omssubadd  34541  carsgclctunlem2  34560  mblfinlem1  38094  ismblfin  38098  ftc1anclem8  38137  ftc1anc  38138  aks6d1c6lem2  42726  aks6d1c6lem3  42727  unitscyglem5  42754  hbtlem2  43639  idomodle  43706  xle2addd  45850  xralrple2  45868  infleinflem1  45883  xralrple4  45886  xralrple3  45887  suplesup2  45889  infleinf2  45926  infxrlesupxr  45948  inficc  46048  limsupequzlem  46234  limsupvaluz2  46250  supcnvlimsup  46252  liminfval2  46280  liminflelimsuplem  46287  limsupgtlem  46289  fourierdlem1  46620  sge0cl  46893  sge0lefi  46910  sge0iunmptlemre  46927  sge0isum  46939  omeunle  47028  omeiunle  47029  caratheodorylem2  47039  hoicvrrex  47068  ovnsubaddlem1  47082  ovolval5lem1  47164  pimdecfgtioo  47229  pimincfltioo  47230