Theorem ltletrd 8586

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

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2200   class class class wbr 4083  ℝcr 8014   < clt 8197   ≤ cle 8198

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4259  ax-pr 4294  ax-un 4525  ax-setind 4630  ax-cnex 8106  ax-resscn 8107  ax-pre-ltwlin 8128

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-xp 4726  df-cnv 4728  df-pnf 8199  df-mnf 8200  df-xr 8201  df-ltxr 8202  df-le 8203

This theorem is referenced by:  lelttrdi  8589  lediv12a  9057  btwnapz  9593  rpgecl  9895  fznatpl1  10289  elfz1b  10303  exbtwnzlemstep  10484  ceiqle  10552  modqabs  10596  mulp1mod1  10604  seq3f1olemqsumk  10751  seqf1oglem1  10758  expgt1  10816  leexp2a  10831  bernneq3  10901  expnbnd  10902  nn0opthlem2d  10960  cvg1nlemres  11517  resqrexlemlo  11545  resqrexlemnmsq  11549  resqrexlemga  11555  abssubap0  11622  icodiamlt  11712  rpmaxcl  11755  reccn2ap  11845  divcnv  12029  cvgratnnlembern  12055  cvgratnnlemabsle  12059  fprodntrivap  12116  efcllemp  12190  sin01bnd  12289  cos01bnd  12290  sin01gt0  12294  cos12dec  12300  eirraplem  12309  dvdslelemd  12375  bitsmod  12488  bitsinv1lem  12493  dvdsbnd  12498  isprm5  12685  1arith  12911  2expltfac  12983  znnen  12990  nninfdclemp1  13042  cnopnap  15306  dedekindeulemlu  15316  suplociccreex  15319  dedekindicclemlu  15325  dedekindicc  15328  ivthinclemlopn  15331  hoverb  15343  limcimolemlt  15359  limccnp2lem  15371  coseq00topi  15530  cosordlem  15544  logdivlti  15576  gausslemma2dlem0c  15751  lgsquadlem1  15777  clwwlkext2edg  16190