Theorem ltletrd 7964

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 7637	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
7	3, 4, 5, 6	syl3anc 1175	. 2 |- ( ph -> ( ( A < B /\ B <_ C ) -> A < C ) )
8	1, 2, 7	mp2and 425	1 |- ( ph -> A < C )

Syntax hints:   -> wi 4   /\ wa 103   e. wcel 1439   class class class wbr 3853   RRcr 7412   < clt 7585   <_ cle 7586

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-bndl 1445  ax-4 1446  ax-13 1450  ax-14 1451  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474  ax-ext 2071  ax-sep 3965  ax-pow 4017  ax-pr 4047  ax-un 4271  ax-setind 4368  ax-cnex 7499  ax-resscn 7500  ax-pre-ltwlin 7521

This theorem depends on definitions:  df-bi 116  df-3an 927  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694  df-eu 1952  df-mo 1953  df-clab 2076  df-cleq 2082  df-clel 2085  df-nfc 2218  df-ne 2257  df-nel 2352  df-ral 2365  df-rex 2366  df-rab 2369  df-v 2624  df-dif 3004  df-un 3006  df-in 3008  df-ss 3015  df-pw 3437  df-sn 3458  df-pr 3459  df-op 3461  df-uni 3662  df-br 3854  df-opab 3908  df-xp 4460  df-cnv 4462  df-pnf 7587  df-mnf 7588  df-xr 7589  df-ltxr 7590  df-le 7591

This theorem is referenced by:  lelttrdi  7967  lediv12a  8418  btwnapz  8939  rpgecl  9225  fznatpl1  9553  elfz1b  9567  exbtwnzlemstep  9722  ceiqle  9783  modqabs  9827  mulp1mod1  9835  seq3f1olemqsumk  9991  expgt1  10056  leexp2a  10071  bernneq3  10139  expnbnd  10140  nn0opthlem2d  10192  cvg1nlemres  10481  resqrexlemlo  10509  resqrexlemnmsq  10513  resqrexlemga  10519  abssubap0  10586  icodiamlt  10676  divcnv  10954  cvgratnnlembern  10980  cvgratnnlemabsle  10984  efcllemp  11011  sin01bnd  11111  cos01bnd  11112  sin01gt0  11115  eirraplem  11127  dvdslelemd  11185  dvdsbnd  11289  znnen  11552