Theorem lelttr 10007

Description: Transitive law. (Contributed by NM, 23-May-1999.)

Assertion

Ref	Expression
lelttr	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Proof of Theorem lelttr

Step	Hyp	Ref	Expression
1		leloe 10003	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
2	1	3adant3 1074	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3		lttr 9993	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
4	3	expd 451	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
5		breq1 4586	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
6	5	biimprd 237	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
8	4, 7	jaod 394	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵) → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
9	2, 8	sylbid 229	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
10	9	impd 446	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Syntax hints:   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   class class class wbr 4583  ℝcr 9814   < clt 9953   ≤ cle 9954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-resscn 9872  ax-pre-lttri 9889  ax-pre-lttrn 9890

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959

This theorem is referenced by:  letr  10010  lelttri  10043  lelttrd  10074  letrp1  10744  ltmul12a  10758  ledivp1  10804  supmul1  10869  bndndx  11168  uzind  11345  fnn0ind  11352  rpnnen1lem5  11694  rpnnen1lem5OLD  11700  xrinfmsslem  12010  elfzo0z  12377  nn0p1elfzo  12378  fzofzim  12382  elfzodifsumelfzo  12401  flge  12468  flflp1  12470  flltdivnn0lt  12496  modfzo0difsn  12604  fsequb  12636  expnlbnd2  12857  ccat2s1fvw  13267  swrdswrd  13312  swrdccatin12lem3  13341  repswswrd  13382  caubnd2  13945  caubnd  13946  mulcn2  14174  cn1lem  14176  rlimo1  14195  o1rlimmul  14197  climsqz  14219  climsqz2  14220  rlimsqzlem  14227  climsup  14248  caucvgrlem2  14253  iseralt  14263  cvgcmp  14389  cvgcmpce  14391  ruclem3  14801  ruclem12  14809  ltoddhalfle  14923  algcvgblem  15128  ncoprmlnprm  15274  pclem  15381  infpn2  15455  gsummoncoe1  19495  mp2pm2mplem4  20433  metss2lem  22126  ngptgp  22250  nghmcn  22359  iocopnst  22547  ovollb2lem  23063  ovolicc2lem4  23095  volcn  23180  ismbf3d  23227  dvcnvrelem1  23584  dvfsumrlim  23598  ulmcn  23957  mtest  23962  logdivlti  24170  isosctrlem1  24348  ftalem2  24600  chtub  24737  bposlem6  24814  gausslemma2dlem2  24892  chtppilim  24964  dchrisumlem3  24980  pntlem3  25098  nvnencycllem  26171  clwlkisclwwlklem2a  26313  vacn  26933  nmcvcn  26934  blocni  27044  chscllem2  27881  lnconi  28276  staddi  28489  stadd3i  28491  ltflcei  32567  poimirlem29  32608  geomcau  32725  heibor1lem  32778  bfplem2  32792  rrncmslem  32801  climinf  38673  leltletr  39940  iccpartigtl  39961  tgoldbach  40232  tgoldbachOLD  40239  zm1nn  40348  clwlkclwwlklem2a  41207  ply1mulgsumlem2  41969  difmodm1lt  42111