Theorem lelttr 11315

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

Assertion

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

Proof of Theorem lelttr

Step	Hyp	Ref	Expression
1		leloe 11311	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
2	1	3adant3 1150	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3		lttr 11301	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
4	3	expd 421	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
5		breq1 5114	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
6	5	biimprd 251	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
8	4, 7	jaod 873	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵) → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
9	2, 8	sylbid 243	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
10	9	impd 416	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146   class class class wbr 5111  ℝcr 11114   < clt 11258   ≤ cle 11259

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pow 5338  ax-pr 5406  ax-un 7742  ax-resscn 11172  ax-pre-lttri 11189  ax-pre-lttrn 11190

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-nel 3067  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-pw 4566  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-er 8700  df-en 8950  df-dom 8951  df-sdom 8952  df-pnf 11260  df-mnf 11261  df-xr 11262  df-ltxr 11263  df-le 11264

This theorem is used by:  leltletr  11316  letr  11319  lelttri  11352  lelttrd  11383  letrp1  12074  ltmul12a  12086  ledivp1  12132  supmul1  12199  bndndx  12518  uzind  12704  fnn0ind  12711  rpnnen1lem5  13021  xrinfmsslem  13350  elfzo0z  13747  nn0p1elfzo  13748  fzofzim  13755  elfzodifsumelfzo  13777  flge  13856  flflp1  13858  flltdivnn0lt  13884  modfzo0difsn  13997  fsequb  14029  expnlbnd2  14288  ccat2s1fvw  14696  swrdswrd  14764  pfxccatin12lem3  14791  repswswrd  14845  caubnd2  15433  caubnd  15434  mulcn2  15671  cn1lem  15673  rlimo1  15692  o1rlimmul  15694  climsqz  15716  climsqz2  15717  rlimsqzlem  15724  climsup  15745  caucvgrlem2  15750  iseralt  15760  cvgcmp  15891  cvgcmpce  15893  ruclem3  16311  ruclem12  16319  ltoddhalfle  16441  algcvgblem  16657  ncoprmlnprm  16809  pclem  16920  infpn2  16995  gsummoncoe1  22518  mp2pm2mplem4  23016  metss2lem  24719  ngptgp  24844  nghmcn  24953  iocopnst  25150  ovollb2lem  25698  ovolicc2lem4  25730  volcn  25816  ismbf3d  25864  dvcnvrelem1  26227  dvfsumrlim  26241  ulmcn  26613  mtest  26618  logdivlti  26836  isosctrlem1  27034  ftalem2  27289  chtub  27427  bposlem6  27504  gausslemma2dlem2  27582  chtppilim  27690  dchrisumlem3  27706  pntlem3  27824  clwlkclwwlklem2a  30416  vacn  31117  nmcvcn  31118  blocni  31228  chscllem2  32061  lnconi  32456  staddi  32669  stadd3i  32671  ltflcei  38316  poimirlem29  38357  geomcau  38468  heibor1lem  38518  bfplem2  38532  rrncmslem  38541  climinf  46380  zm1nn  48097  muldvdsfacgt  48181  muldvdsfacm1  48182  iccpartigtl  48230  tgoldbach  48640  ply1mulgsumlem2  49224