Theorem ltletrd 8379

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 8046	. . 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 7991   <_ cle 7992

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 7993  df-mnf 7994  df-xr 7995  df-ltxr 7996  df-le 7997

This theorem is referenced by:  lelttrdi  8382  lediv12a  8850  btwnapz  9382  rpgecl  9681  fznatpl1  10075  elfz1b  10089  exbtwnzlemstep  10247  ceiqle  10312  modqabs  10356  mulp1mod1  10364  seq3f1olemqsumk  10498  expgt1  10557  leexp2a  10572  bernneq3  10642  expnbnd  10643  nn0opthlem2d  10700  cvg1nlemres  10993  resqrexlemlo  11021  resqrexlemnmsq  11025  resqrexlemga  11031  abssubap0  11098  icodiamlt  11188  rpmaxcl  11231  reccn2ap  11320  divcnv  11504  cvgratnnlembern  11530  cvgratnnlemabsle  11534  fprodntrivap  11591  efcllemp  11665  sin01bnd  11764  cos01bnd  11765  sin01gt0  11768  cos12dec  11774  eirraplem  11783  dvdslelemd  11848  dvdsbnd  11956  isprm5  12141  1arith  12364  znnen  12398  nninfdclemp1  12450  cnopnap  14064  dedekindeulemlu  14069  suplociccreex  14072  dedekindicclemlu  14078  dedekindicc  14081  ivthinclemlopn  14084  limcimolemlt  14103  limccnp2lem  14115  coseq00topi  14226  cosordlem  14240  logdivlti  14272