Theorem ltletr 11242

Description: Transitive law. (Contributed by NM, 25-Aug-1999.)

Assertion

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

Proof of Theorem ltletr

Step	Hyp	Ref	Expression
1		leloe 11236	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
2	1	3adant1 1130	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 ↔ (𝐵 < 𝐶 ∨ 𝐵 = 𝐶)))
3		lttr 11226	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 < 𝐶) → 𝐴 < 𝐶))
4	3	expcomd 416	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 < 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
5		breq2 5106	. . . . . 6 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 ↔ 𝐴 < 𝐶))
6	5	biimpd 229	. . . . 5 ⊢ (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶))
7	6	a1i 11	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 = 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
8	4, 7	jaod 859	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐵 < 𝐶 ∨ 𝐵 = 𝐶) → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
9	2, 8	sylbid 240	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 ≤ 𝐶 → (𝐴 < 𝐵 → 𝐴 < 𝐶)))
10	9	impcomd 411	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 < 𝐵 ∧ 𝐵 ≤ 𝐶) → 𝐴 < 𝐶))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   class class class wbr 5102  ℝcr 11043   < clt 11184   ≤ cle 11185

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 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-resscn 11101  ax-pre-lttri 11118  ax-pre-lttrn 11119

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190

This theorem is referenced by:  ltleletr  11243  ltletri  11278  ltletrd  11310  ltleadd  11637  lediv12a  12052  nngt0  12193  nnrecgt0  12205  elnnnn0c  12463  elnnz1  12535  zltp1le  12559  uz3m2nn  12829  zbtwnre  12881  ledivge1le  13000  addlelt  13043  qbtwnre  13135  xlemul1a  13224  xrsupsslem  13243  zltaddlt1le  13442  elfzodifsumelfzo  13668  ssfzo12bi  13698  elfznelfzo  13709  ceile  13787  swrdswrd  14646  swrdccatin1  14666  repswswrd  14725  01sqrexlem4  15187  resqrex  15192  caubnd  15301  rlim2lt  15439  cos01gt0  16135  ruclem12  16185  oddge22np1  16295  sadcaddlem  16403  nn0seqcvgd  16516  coprm  16657  prmgaplem7  17004  prmlem1  17054  prmlem2  17066  icoopnst  24812  ovollb2lem  25365  dvcnvrelem1  25898  aaliou  26222  tanord  26423  logdivlti  26505  logdivlt  26506  ftalem2  26960  gausslemma2dlem1a  27252  pntlem3  27496  crctcshwlkn0lem3  29715  nn0prpwlem  36283  isbasisrelowllem1  37316  isbasisrelowllem2  37317  ltflcei  37575  tan2h  37579  poimirlem29  37616  poimirlem32  37619  stoweidlem26  45997  stoweid  46034  2leaddle2  47272  gbegt5  47735  gbowgt5  47736  sgoldbeven3prm  47757  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  evengpoap3  47773  bgoldbnnsum3prm  47778  cznnring  48223  nn0sumltlt  48311  rege1logbrege0  48520  rege1logbzge0  48521  fllog2  48530  dignn0ldlem  48564