Theorem ltletrd 8516

Description: Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)

Hypotheses

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

Assertion

Ref	Expression
ltletrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem ltletrd

Step	Hyp	Ref	Expression
1		ltletrd.4	. 2 ⊢ (𝜑 → 𝐴 < 𝐵)
2		ltletrd.5	. 2 ⊢ (𝜑 → 𝐵 ≤ 𝐶)
3		ltadd2d.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltadd2d.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		ltadd2d.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		ltletr 8182	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1250	. 2 ⊢ (𝜑 → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 433	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2177   class class class wbr 4051  ℝcr 7944   < clt 8127   ≤ cle 8128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 711  ax-5 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-10 1529  ax-11 1530  ax-i12 1531  ax-bndl 1533  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-13 2179  ax-14 2180  ax-ext 2188  ax-sep 4170  ax-pow 4226  ax-pr 4261  ax-un 4488  ax-setind 4593  ax-cnex 8036  ax-resscn 8037  ax-pre-ltwlin 8058

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-fal 1379  df-nf 1485  df-sb 1787  df-eu 2058  df-mo 2059  df-clab 2193  df-cleq 2199  df-clel 2202  df-nfc 2338  df-ne 2378  df-nel 2473  df-ral 2490  df-rex 2491  df-rab 2494  df-v 2775  df-dif 3172  df-un 3174  df-in 3176  df-ss 3183  df-pw 3623  df-sn 3644  df-pr 3645  df-op 3647  df-uni 3857  df-br 4052  df-opab 4114  df-xp 4689  df-cnv 4691  df-pnf 8129  df-mnf 8130  df-xr 8131  df-ltxr 8132  df-le 8133

This theorem is referenced by:  lelttrdi  8519  lediv12a  8987  btwnapz  9523  rpgecl  9824  fznatpl1  10218  elfz1b  10232  exbtwnzlemstep  10412  ceiqle  10480  modqabs  10524  mulp1mod1  10532  seq3f1olemqsumk  10679  seqf1oglem1  10686  expgt1  10744  leexp2a  10759  bernneq3  10829  expnbnd  10830  nn0opthlem2d  10888  cvg1nlemres  11371  resqrexlemlo  11399  resqrexlemnmsq  11403  resqrexlemga  11409  abssubap0  11476  icodiamlt  11566  rpmaxcl  11609  reccn2ap  11699  divcnv  11883  cvgratnnlembern  11909  cvgratnnlemabsle  11913  fprodntrivap  11970  efcllemp  12044  sin01bnd  12143  cos01bnd  12144  sin01gt0  12148  cos12dec  12154  eirraplem  12163  dvdslelemd  12229  bitsmod  12342  bitsinv1lem  12347  dvdsbnd  12352  isprm5  12539  1arith  12765  2expltfac  12837  znnen  12844  nninfdclemp1  12896  cnopnap  15158  dedekindeulemlu  15168  suplociccreex  15171  dedekindicclemlu  15177  dedekindicc  15180  ivthinclemlopn  15183  hoverb  15195  limcimolemlt  15211  limccnp2lem  15223  coseq00topi  15382  cosordlem  15396  logdivlti  15428  gausslemma2dlem0c  15603  lgsquadlem1  15629