Theorem ltletrd 8378

Description: Transitive law deduction for 'less than', 'less than or equal to'. (Contributed by NM, 9-Jan-2006.)

Hypotheses

Ref	Expression
ltadd2d.1	|- ( ph -> A e. RR )
ltadd2d.2	|- ( ph -> B e. RR )
ltadd2d.3	|- ( ph -> C e. RR )
ltletrd.4	|- ( ph -> A < B )
ltletrd.5	|- ( ph -> B <_ C )

Assertion

Ref	Expression
ltletrd	|- ( ph -> A < C )

Proof of Theorem ltletrd

Step	Hyp	Ref	Expression
1		ltletrd.4	. 2 |- ( ph -> A < B )
2		ltletrd.5	. 2 |- ( ph -> B <_ C )
3		ltadd2d.1	. . 3 |- ( ph -> A e. RR )
4		ltadd2d.2	. . 3 |- ( ph -> B e. RR )
5		ltadd2d.3	. . 3 |- ( ph -> C e. RR )
6		ltletr 8045	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
7	3, 4, 5, 6	syl3anc 1238	. 2 |- ( ph -> ( ( A < B /\ B <_ C ) -> A < C ) )
8	1, 2, 7	mp2and 433	1 |- ( ph -> A < C )

Syntax hints:   -> wi 4   /\ wa 104   e. wcel 2148   class class class wbr 4003   RRcr 7809   < clt 7990   <_ cle 7991

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536  ax-cnex 7901  ax-resscn 7902  ax-pre-ltwlin 7923

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-rab 2464  df-v 2739  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-br 4004  df-opab 4065  df-xp 4632  df-cnv 4634  df-pnf 7992  df-mnf 7993  df-xr 7994  df-ltxr 7995  df-le 7996

This theorem is referenced by:  lelttrdi  8381  lediv12a  8849  btwnapz  9381  rpgecl  9680  fznatpl1  10073  elfz1b  10087  exbtwnzlemstep  10245  ceiqle  10310  modqabs  10354  mulp1mod1  10362  seq3f1olemqsumk  10496  expgt1  10555  leexp2a  10570  bernneq3  10639  expnbnd  10640  nn0opthlem2d  10696  cvg1nlemres  10989  resqrexlemlo  11017  resqrexlemnmsq  11021  resqrexlemga  11027  abssubap0  11094  icodiamlt  11184  rpmaxcl  11227  reccn2ap  11316  divcnv  11500  cvgratnnlembern  11526  cvgratnnlemabsle  11530  fprodntrivap  11587  efcllemp  11661  sin01bnd  11760  cos01bnd  11761  sin01gt0  11764  cos12dec  11770  eirraplem  11779  dvdslelemd  11843  dvdsbnd  11951  isprm5  12136  1arith  12359  znnen  12393  nninfdclemp1  12445  cnopnap  13987  dedekindeulemlu  13992  suplociccreex  13995  dedekindicclemlu  14001  dedekindicc  14004  ivthinclemlopn  14007  limcimolemlt  14026  limccnp2lem  14038  coseq00topi  14149  cosordlem  14163  logdivlti  14195