Theorem lelttr 10584

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

Assertion

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

Proof of Theorem lelttr

Step	Hyp	Ref	Expression
1		leloe 10580	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
2	1	3adant3 1125	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 ↔ (𝐴 < 𝐵 ∨ 𝐴 = 𝐵)))
3		lttr 10570	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
4	3	expd 416	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
5		breq1 4971	. . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 < 𝐶 ↔ 𝐵 < 𝐶))
6	5	biimprd 249	. . . . 5 ⊢ (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 = 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
8	4, 7	jaod 854	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∨ 𝐴 = 𝐵) → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
9	2, 8	sylbid 241	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 ≤ 𝐵 → (𝐵 < 𝐶 → 𝐴 < 𝐶)))
10	9	impd 411	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 ≤ 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 842   ∧ w3a 1080   = wceq 1525   ∈ wcel 2083   class class class wbr 4968  ℝcr 10389   < clt 10528   ≤ cle 10529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-13 2346  ax-ext 2771  ax-sep 5101  ax-nul 5108  ax-pow 5164  ax-pr 5228  ax-un 7326  ax-resscn 10447  ax-pre-lttri 10464  ax-pre-lttrn 10465

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ne 2987  df-nel 3093  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3442  df-sbc 3712  df-csb 3818  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-if 4388  df-pw 4461  df-sn 4479  df-pr 4481  df-op 4485  df-uni 4752  df-br 4969  df-opab 5031  df-mpt 5048  df-id 5355  df-xp 5456  df-rel 5457  df-cnv 5458  df-co 5459  df-dm 5460  df-rn 5461  df-res 5462  df-ima 5463  df-iota 6196  df-fun 6234  df-fn 6235  df-f 6236  df-f1 6237  df-fo 6238  df-f1o 6239  df-fv 6240  df-er 8146  df-en 8365  df-dom 8366  df-sdom 8367  df-pnf 10530  df-mnf 10531  df-xr 10532  df-ltxr 10533  df-le 10534

This theorem is referenced by:  letr  10587  lelttri  10620  lelttrd  10651  letrp1  11338  ltmul12a  11350  ledivp1  11396  supmul1  11464  bndndx  11750  uzind  11928  fnn0ind  11935  rpnnen1lem5  12234  xrinfmsslem  12555  elfzo0z  12933  nn0p1elfzo  12934  fzofzim  12938  elfzodifsumelfzo  12957  flge  13029  flflp1  13031  flltdivnn0lt  13057  modfzo0difsn  13165  fsequb  13197  expnlbnd2  13449  ccat2s1fvw  13840  swrdswrd  13907  pfxccatin12lem3  13934  repswswrd  13986  caubnd2  14555  caubnd  14556  mulcn2  14790  cn1lem  14792  rlimo1  14811  o1rlimmul  14813  climsqz  14835  climsqz2  14836  rlimsqzlem  14843  climsup  14864  caucvgrlem2  14869  iseralt  14879  cvgcmp  15008  cvgcmpce  15010  ruclem3  15423  ruclem12  15431  ltoddhalfle  15547  algcvgblem  15754  ncoprmlnprm  15901  pclem  16008  infpn2  16082  gsummoncoe1  20159  mp2pm2mplem4  21105  metss2lem  22808  ngptgp  22932  nghmcn  23041  iocopnst  23231  ovollb2lem  23776  ovolicc2lem4  23808  volcn  23894  ismbf3d  23942  dvcnvrelem1  24301  dvfsumrlim  24315  ulmcn  24674  mtest  24679  logdivlti  24888  isosctrlem1  25081  ftalem2  25337  chtub  25474  bposlem6  25551  gausslemma2dlem2  25629  chtppilim  25737  dchrisumlem3  25753  pntlem3  25871  clwlkclwwlklem2a  27462  vacn  28158  nmcvcn  28159  blocni  28269  chscllem2  29102  lnconi  29497  staddi  29710  stadd3i  29712  ltflcei  34432  poimirlem29  34473  geomcau  34587  heibor1lem  34640  bfplem2  34654  rrncmslem  34663  climinf  41450  leltletr  43031  zm1nn  43040  iccpartigtl  43087  tgoldbach  43486  ply1mulgsumlem2  43943  difmodm1lt  44085