Theorem lelttrd 8111

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

Hypotheses

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

Assertion

Ref	Expression
lelttrd	⊢ (𝜑 → 𝐴 < 𝐶)

Proof of Theorem lelttrd

Step	Hyp	Ref	Expression
1		lelttrd.4	. 2 ⊢ (𝜑 → 𝐴 ≤ 𝐵)
2		lelttrd.5	. 2 ⊢ (𝜑 → 𝐵 < 𝐶)
3		ltd.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ ℝ)
4		ltd.2	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℝ)
5		letrd.3	. . 3 ⊢ (𝜑 → 𝐶 ∈ ℝ)
6		lelttr 8075	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
7	3, 4, 5, 6	syl3anc 1249	. 2 ⊢ (𝜑 → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
8	1, 2, 7	mp2and 433	1 ⊢ (𝜑 → 𝐴 < 𝐶)

Syntax hints:   → wi 4   ∧ wa 104   ∈ wcel 2160   class class class wbr 4018  ℝcr 7839   < clt 8021   ≤ cle 8022

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4192  ax-pr 4227  ax-un 4451  ax-setind 4554  ax-cnex 7931  ax-resscn 7932  ax-pre-ltwlin 7953

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-rab 2477  df-v 2754  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-xp 4650  df-cnv 4652  df-pnf 8023  df-mnf 8024  df-xr 8025  df-ltxr 8026  df-le 8027

This theorem is referenced by:  lt2msq1  8871  ledivp1  8889  suprzclex  9380  btwnapz  9412  ge0p1rp  9714  elfzolt3  10186  exbtwnz  10280  btwnzge0  10330  flltdivnn0lt  10334  modqid  10379  mulqaddmodid  10394  modqsubdir  10423  nn0opthlem2d  10732  bcp1nk  10773  zfz1isolemiso  10850  resqrexlemover  11050  resqrexlemnm  11058  resqrexlemcvg  11059  resqrexlemglsq  11062  resqrexlemga  11063  abslt  11128  abs3lem  11151  fzomaxdiflem  11152  icodiamlt  11220  maxltsup  11258  reccn2ap  11352  expcnvre  11542  absltap  11548  cvgratnnlemfm  11568  cvgratnnlemrate  11569  mertenslemi1  11574  ef01bndlem  11795  sin01bnd  11796  cos01bnd  11797  eirraplem  11815  dvdslelemd  11880  isprm5lem  12172  sqrt2irrap  12211  eulerthlemrprm  12260  eulerthlema  12261  pcfaclem  12380  pockthg  12388  4sqlem11  12432  4sqlem12  12433  4sqlem13m  12434  ssblex  14383  dedekindeulemuub  14547  dedekindeulemlu  14551  suplociccreex  14554  dedekindicclemuub  14556  dedekindicclemlu  14560  dedekindicc  14563  ivthinclemuopn  14568  dveflem  14639  coseq00topi  14708  coseq0negpitopi  14709  cosordlem  14722  logbgcd1irraplemexp  14838  lgsdirprm  14888  2sqlem8  14923  qdencn  15229  cvgcmp2nlemabs  15234