Theorem ltletrd 8581

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 8247	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )
7	3, 4, 5, 6	syl3anc 1271	. 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 2200   class class class wbr 4083   RRcr 8009   < clt 8192   <_ cle 8193

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4202  ax-pow 4258  ax-pr 4293  ax-un 4524  ax-setind 4629  ax-cnex 8101  ax-resscn 8102  ax-pre-ltwlin 8123

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-rab 2517  df-v 2801  df-dif 3199  df-un 3201  df-in 3203  df-ss 3210  df-pw 3651  df-sn 3672  df-pr 3673  df-op 3675  df-uni 3889  df-br 4084  df-opab 4146  df-xp 4725  df-cnv 4727  df-pnf 8194  df-mnf 8195  df-xr 8196  df-ltxr 8197  df-le 8198

This theorem is referenced by:  lelttrdi  8584  lediv12a  9052  btwnapz  9588  rpgecl  9890  fznatpl1  10284  elfz1b  10298  exbtwnzlemstep  10479  ceiqle  10547  modqabs  10591  mulp1mod1  10599  seq3f1olemqsumk  10746  seqf1oglem1  10753  expgt1  10811  leexp2a  10826  bernneq3  10896  expnbnd  10897  nn0opthlem2d  10955  cvg1nlemres  11512  resqrexlemlo  11540  resqrexlemnmsq  11544  resqrexlemga  11550  abssubap0  11617  icodiamlt  11707  rpmaxcl  11750  reccn2ap  11840  divcnv  12024  cvgratnnlembern  12050  cvgratnnlemabsle  12054  fprodntrivap  12111  efcllemp  12185  sin01bnd  12284  cos01bnd  12285  sin01gt0  12289  cos12dec  12295  eirraplem  12304  dvdslelemd  12370  bitsmod  12483  bitsinv1lem  12488  dvdsbnd  12493  isprm5  12680  1arith  12906  2expltfac  12978  znnen  12985  nninfdclemp1  13037  cnopnap  15301  dedekindeulemlu  15311  suplociccreex  15314  dedekindicclemlu  15320  dedekindicc  15323  ivthinclemlopn  15326  hoverb  15338  limcimolemlt  15354  limccnp2lem  15366  coseq00topi  15525  cosordlem  15539  logdivlti  15571  gausslemma2dlem0c  15746  lgsquadlem1  15772  clwwlkext2edg  16164