Theorem lelttr 11351

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

Assertion

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

Proof of Theorem lelttr

Step	Hyp	Ref	Expression
1		leloe 11347	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
2	1	3adant3 1133	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3		lttr 11337	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
4	3	expd 415	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
5		breq1 5146	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
6	5	biimprd 248	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
8	4, 7	jaod 860	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵) → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
9	2, 8	sylbid 240	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
10	9	impd 410	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1540   ∈ wcel 2108   class class class wbr 5143  ℝcr 11154   < clt 11295   ≤ cle 11296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-resscn 11212  ax-pre-lttri 11229  ax-pre-lttrn 11230

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301

This theorem is referenced by:  leltletr  11352  letr  11355  lelttri  11388  lelttrd  11419  letrp1  12111  ltmul12a  12123  ledivp1  12170  supmul1  12237  bndndx  12525  uzind  12710  fnn0ind  12717  rpnnen1lem5  13023  xrinfmsslem  13350  elfzo0z  13741  nn0p1elfzo  13742  fzofzim  13749  elfzodifsumelfzo  13770  flge  13845  flflp1  13847  flltdivnn0lt  13873  modfzo0difsn  13984  fsequb  14016  expnlbnd2  14273  ccat2s1fvw  14676  swrdswrd  14743  pfxccatin12lem3  14770  repswswrd  14822  caubnd2  15396  caubnd  15397  mulcn2  15632  cn1lem  15634  rlimo1  15653  o1rlimmul  15655  climsqz  15677  climsqz2  15678  rlimsqzlem  15685  climsup  15706  caucvgrlem2  15711  iseralt  15721  cvgcmp  15852  cvgcmpce  15854  ruclem3  16269  ruclem12  16277  ltoddhalfle  16398  algcvgblem  16614  ncoprmlnprm  16765  pclem  16876  infpn2  16951  gsummoncoe1  22312  mp2pm2mplem4  22815  metss2lem  24524  ngptgp  24649  nghmcn  24766  iocopnst  24970  ovollb2lem  25523  ovolicc2lem4  25555  volcn  25641  ismbf3d  25689  dvcnvrelem1  26056  dvfsumrlim  26072  ulmcn  26442  mtest  26447  logdivlti  26662  isosctrlem1  26861  ftalem2  27117  chtub  27256  bposlem6  27333  gausslemma2dlem2  27411  chtppilim  27519  dchrisumlem3  27535  pntlem3  27653  clwlkclwwlklem2a  30017  vacn  30713  nmcvcn  30714  blocni  30824  chscllem2  31657  lnconi  32052  staddi  32265  stadd3i  32267  ltflcei  37615  poimirlem29  37656  geomcau  37766  heibor1lem  37816  bfplem2  37830  rrncmslem  37839  climinf  45621  zm1nn  47314  iccpartigtl  47410  tgoldbach  47804  ply1mulgsumlem2  48304  difmodm1lt  48443