Theorem xrltletrd 12734

Description: Transitive law for ordering on extended reals. (Contributed by Mario Carneiro, 23-Aug-2015.)

Hypotheses

Ref	Expression
xrlttrd.1	⊢ (𝜑 → 𝐴 ∈ ℝ*)
xrlttrd.2	⊢ (𝜑 → 𝐵 ∈ ℝ*)
xrlttrd.3	⊢ (𝜑 → 𝐶 ∈ ℝ*)
xrltletrd.4	⊢ (𝜑 → 𝐴 < 𝐵)
xrltletrd.5	⊢ (𝜑 → 𝐵 ≤ 𝐶)

Assertion

Ref	Expression
xrltletrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem xrltletrd

Step	Hyp	Ref	Expression
1		xrltletrd.4	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		xrltletrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		xrlttrd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ*)
4		xrlttrd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ*)
5		xrlttrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ*)
6		xrltletr 12730	. . 3 ⊢ ((𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1373	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 699	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110   class class class wbr 5043  ℝ^*cxr 10849   < clt 10850   ≤ cle 10851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2706  ax-sep 5181  ax-nul 5188  ax-pow 5247  ax-pr 5311  ax-un 7512  ax-cnex 10768  ax-resscn 10769  ax-pre-lttri 10786  ax-pre-lttrn 10787

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2537  df-eu 2566  df-clab 2713  df-cleq 2726  df-clel 2812  df-nfc 2882  df-ne 2936  df-nel 3040  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3403  df-sbc 3688  df-csb 3803  df-dif 3860  df-un 3862  df-in 3864  df-ss 3874  df-nul 4228  df-if 4430  df-pw 4505  df-sn 4532  df-pr 4534  df-op 4538  df-uni 4810  df-br 5044  df-opab 5106  df-mpt 5125  df-id 5444  df-po 5457  df-so 5458  df-xp 5546  df-rel 5547  df-cnv 5548  df-co 5549  df-dm 5550  df-rn 5551  df-res 5552  df-ima 5553  df-iota 6327  df-fun 6371  df-fn 6372  df-f 6373  df-f1 6374  df-fo 6375  df-f1o 6376  df-fv 6377  df-er 8380  df-en 8616  df-dom 8617  df-sdom 8618  df-pnf 10852  df-mnf 10853  df-xr 10854  df-ltxr 10855  df-le 10856

This theorem is referenced by:  xlt2add  12833  xadddi2  12870  supxrre  12900  infxrre  12909  ixxlb  12940  elicore  12970  elico2  12982  elicc2  12983  caucvgrlem  15219  isnzr2hash  20274  xrsdsreclblem  20381  xblss2ps  23271  xblss2  23272  tgioo  23665  xrge0tsms  23703  xrhmeo  23815  ovoliunlem1  24371  ovoliun  24374  ioombl1lem2  24428  vitalilem4  24480  itg2monolem2  24621  itg2gt0  24630  dvferm1lem  24853  dvferm2lem  24855  lhop1lem  24882  pserdvlem2  25292  abelthlem3  25297  logtayl  25520  xrge0tsmsd  31008  esum2d  31745  usgrcyclgt2v  32778  relowlssretop  35228  itg2gt0cn  35526  areacirclem5  35563  xrge0nemnfd  42496  supxrgere  42497  supxrgelem  42501  infrpge  42515  xrralrecnnge  42555  supxrunb3  42564  icoopn  42690  limsupre  42811  limsupre3lem  42902  xlimpnfv  43008  fourierdlem27  43304  fourierdlem87  43363  gsumge0cl  43538  sge0pr  43561  sge0ssre  43564  sge0xaddlem1  43600  meaiuninc3v  43651  pimiooltgt  43874  pimdecfgtioc  43878  preimageiingt  43883