MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lttri Unicode version

Theorem lttri 8913
Description: 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.)
Hypotheses
Ref Expression
lt.1  |-  A  e.  RR
lt.2  |-  B  e.  RR
lt.3  |-  C  e.  RR
Assertion
Ref Expression
lttri  |-  ( ( A  <  B  /\  B  <  C )  ->  A  <  C )

Proof of Theorem lttri
StepHypRef Expression
1 lt.1 . 2  |-  A  e.  RR
2 lt.2 . 2  |-  B  e.  RR
3 lt.3 . 2  |-  C  e.  RR
4 lttr 8867 . 2  |-  ( ( A  e.  RR  /\  B  e.  RR  /\  C  e.  RR )  ->  (
( A  <  B  /\  B  <  C )  ->  A  <  C
) )
51, 2, 3, 4mp3an 1282 1  |-  ( ( A  <  B  /\  B  <  C )  ->  A  <  C )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    e. wcel 1621   class class class wbr 3997   RRcr 8704    < clt 8835
This theorem is referenced by:  1lt3  9856  2lt4  9858  1lt4  9859  3lt5  9861  2lt5  9862  1lt5  9863  4lt6  9865  3lt6  9866  2lt6  9867  1lt6  9868  5lt7  9870  4lt7  9871  3lt7  9872  2lt7  9873  1lt7  9874  6lt8  9876  5lt8  9877  4lt8  9878  3lt8  9879  2lt8  9880  1lt8  9881  7lt9  9883  6lt9  9884  5lt9  9885  4lt9  9886  3lt9  9887  2lt9  9888  1lt9  9889  8lt10  9891  7lt10  9892  6lt10  9893  5lt10  9894  4lt10  9895  3lt10  9896  2lt10  9897  1lt10  9898  sincos2sgn  12437  epos  12448  dvdslelem  12536  oppcbas  13584  sralem  15893  zlmlem  16434  tnglem  18119  xrhmph  18408  vitalilem4  18929  pipos  19796  logneg  19904  asin1  20153  reasinsin  20155  atan1  20187  bposlem8  20493  bposlem9  20494  chebbnd1lem2  20582  chebbnd1lem3  20583  chebbnd1  20584  mulog2sumlem2  20647  pntibndlem1  20701  pntlemb  20709  pntlemk  20718  axlowdimlem16  23961  fdc  25823
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pow 4160  ax-pr 4186  ax-un 4484  ax-resscn 8762  ax-pre-lttrn 8780
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-nel 2424  df-ral 2523  df-rex 2524  df-rab 2527  df-v 2765  df-sbc 2967  df-csb 3057  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-pw 3601  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-mpt 4053  df-id 4281  df-xp 4675  df-rel 4676  df-cnv 4677  df-co 4678  df-dm 4679  df-rn 4680  df-res 4681  df-ima 4682  df-fun 4683  df-fn 4684  df-f 4685  df-f1 4686  df-fo 4687  df-f1o 4688  df-fv 4689  df-er 6628  df-en 6832  df-dom 6833  df-sdom 6834  df-pnf 8837  df-mnf 8838  df-ltxr 8840
  Copyright terms: Public domain W3C validator