Theorem letrd 8143

Description: Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.)

Hypotheses

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

Assertion

Ref	Expression
letrd	|- ( ph -> A <_ C )

Proof of Theorem letrd

Step	Hyp	Ref	Expression
1		letrd.4	. 2 |- ( ph -> A <_ B )
2		letrd.5	. 2 |- ( ph -> B <_ C )
3		ltd.1	. . 3 |- ( ph -> A e. RR )
4		ltd.2	. . 3 |- ( ph -> B e. RR )
5		letrd.3	. . 3 |- ( ph -> C e. RR )
6		letr 8102	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )
7	3, 4, 5, 6	syl3anc 1249	. 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 2164   class class class wbr 4029   RRcr 7871   <_ cle 8055

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 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2166  ax-14 2167  ax-ext 2175  ax-sep 4147  ax-pow 4203  ax-pr 4238  ax-un 4464  ax-setind 4569  ax-cnex 7963  ax-resscn 7964  ax-pre-ltwlin 7985

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2045  df-mo 2046  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-ne 2365  df-nel 2460  df-ral 2477  df-rex 2478  df-rab 2481  df-v 2762  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pw 3603  df-sn 3624  df-pr 3625  df-op 3627  df-uni 3836  df-br 4030  df-opab 4091  df-xp 4665  df-cnv 4667  df-pnf 8056  df-mnf 8057  df-xr 8058  df-ltxr 8059  df-le 8060

This theorem is referenced by:  nn0negleid  9385  eluzuzle  9600  infregelbex  9663  fzdisj  10118  difelfzle  10200  flqwordi  10357  btwnzge0  10369  fldiv4lem1div2uz2  10375  flqleceil  10388  modqltm1p1mod  10447  seq3split  10559  iseqf1olemqcl  10570  iseqf1olemnab  10572  iseqf1olemab  10573  seq3f1olemqsumkj  10582  seq3f1olemqsumk  10583  seq3f1olemqsum  10584  seqf1oglem1  10590  seqfeq4g  10602  bernneq  10731  bernneq3  10733  zzlesq  10779  nn0opthlem2d  10792  faclbnd  10812  facubnd  10816  seq3coll  10913  resqrexlemover  11154  resqrexlemdecn  11156  resqrexlemcalc3  11160  absle  11233  releabs  11240  maxleastb  11358  climsqz  11478  climsqz2  11479  fsum3cvg3  11539  expcnvap0  11645  geolim2  11655  cvgratnnlemabsle  11670  cvgratnnlemfm  11672  cvgratnnlemrate  11673  cvgratz  11675  mertenslem2  11679  eftlub  11833  cos12dec  11911  divalglemnqt  12061  infssuzex  12086  suprzubdc  12089  ncoprmgcdne1b  12227  prmdc  12268  isprm5lem  12279  eulerthlemrprm  12367  eulerthlema  12368  pcmpt2  12482  pcfac  12488  4sqexercise2  12537  4sqlemsdc  12538  4sqlem11  12539  ennnfoneleminc  12568  ennnfonelemkh  12569  nninfdclemlt  12608  strleund  12721  strext  12723  gsumfzfsumlemm  14075  psrbaglesuppg  14158  suplociccex  14779  ivthinclemlopn  14790  ivthinclemuopn  14792  dveflem  14872  cosordlem  14984  rpabscxpbnd  15073  lgsdirprm  15150  lgsquadlem1  15191  2sqlem8  15210