Theorem letrd 7605

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

Syntax hints:   -> wi 4   /\ wa 102   e. wcel 1438   class class class wbr 3845   RRcr 7347   <_ cle 7521

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-13 1449  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3957  ax-pow 4009  ax-pr 4036  ax-un 4260  ax-setind 4353  ax-cnex 7434  ax-resscn 7435  ax-pre-ltwlin 7456

This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ne 2256  df-nel 2351  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-dif 3001  df-un 3003  df-in 3005  df-ss 3012  df-pw 3431  df-sn 3452  df-pr 3453  df-op 3455  df-uni 3654  df-br 3846  df-opab 3900  df-xp 4444  df-cnv 4446  df-pnf 7522  df-mnf 7523  df-xr 7524  df-ltxr 7525  df-le 7526

This theorem is referenced by:  eluzuzle  9025  fzdisj  9464  difelfzle  9541  flqwordi  9691  btwnzge0  9703  flqleceil  9720  modqltm1p1mod  9779  seq3split  9903  iseqf1olemqcl  9911  iseqf1olemnab  9913  iseqf1olemab  9914  seq3f1olemqsumkj  9923  seq3f1olemqsumk  9924  seq3f1olemqsum  9925  bernneq  10070  bernneq3  10072  nn0opthlem2d  10125  faclbnd  10145  facubnd  10149  iseqcoll  10243  resqrexlemover  10439  resqrexlemdecn  10441  resqrexlemcalc3  10445  absle  10518  releabs  10525  maxleastb  10643  climsqz  10719  climsqz2  10720  fsum3cvg3  10785  expcnvap0  10892  geolim2  10902  cvgratnnlemabsle  10917  cvgratnnlemfm  10919  cvgratnnlemrate  10920  cvgratz  10922  mertenslem2  10926  eftlub  10976  divalglemnqt  11194  infssuzex  11219  ncoprmgcdne1b  11345