Theorem xrletrd 13067

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   class class class wbr 5095  ℝ^*cxr 11156   ≤ cle 11158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pow 5307  ax-pr 5374  ax-un 7677  ax-cnex 11073  ax-resscn 11074  ax-pre-lttri 11091  ax-pre-lttrn 11092

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-nel 3034  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5516  df-po 5529  df-so 5530  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497  df-er 8631  df-en 8880  df-dom 8881  df-sdom 8882  df-pnf 11159  df-mnf 11160  df-xr 11161  df-ltxr 11162  df-le 11163

This theorem is referenced by:  xaddge0  13164  ixxub  13273  ixxlb  13274  limsupval2  15394  0ram  16939  xpsdsval  24316  xblss2ps  24336  xblss2  24337  comet  24448  stdbdxmet  24450  nmoleub  24666  metnrmlem1  24795  nmoleub2lem  25061  ovollb2lem  25436  ovoliunlem2  25451  ovolscalem1  25461  ovolicc1  25464  ovolicc2lem4  25468  voliunlem2  25499  uniioombllem3  25533  itg2uba  25691  itg2lea  25692  itg2split  25697  itg2monolem3  25700  itg2gt0  25708  lhop1lem  25965  dvfsumlem2  25980  dvfsumlem2OLD  25981  dvfsumlem3  25982  dvfsumlem4  25983  deg1addle2  26054  deg1sublt  26062  nmooge0  30768  ply1degltlss  33605  metideq  33978  measiun  34303  omssubadd  34385  carsgclctunlem2  34404  mblfinlem1  37770  ismblfin  37774  ftc1anclem8  37813  ftc1anc  37814  aks6d1c6lem2  42337  aks6d1c6lem3  42338  unitscyglem5  42365  hbtlem2  43281  idomodle  43348  xle2addd  45497  xralrple2  45515  infleinflem1  45530  xralrple4  45533  xralrple3  45534  suplesup2  45536  infleinf2  45574  infxrlesupxr  45596  inficc  45696  limsupequzlem  45882  limsupvaluz2  45898  supcnvlimsup  45900  liminfval2  45928  liminflelimsuplem  45935  limsupgtlem  45937  fourierdlem1  46268  sge0cl  46541  sge0lefi  46558  sge0iunmptlemre  46575  sge0isum  46587  omeunle  46676  omeiunle  46677  caratheodorylem2  46687  hoicvrrex  46716  ovnsubaddlem1  46730  ovolval5lem1  46812  pimdecfgtioo  46877  pimincfltioo  46878