Theorem letrd 10194

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

Syntax hints:   -> wi 4   /\ wa 384   e. wcel 1990   class class class wbr 4653   RRcr 9935   <_ cle 10075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-resscn 9993  ax-pre-lttri 10010  ax-pre-lttrn 10011

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080

This theorem is referenced by:  lesub3d  10645  supmul1  10992  supmul  10995  nn0negleid  11345  eluzuzle  11696  iccsplit  12305  supicc  12320  fzdisj  12368  ssfzunsnext  12386  difelfzle  12452  flwordi  12613  flleceil  12652  uzsup  12662  modltm1p1mod  12722  seqf1olem1  12840  bernneq  12990  bernneq3  12992  discr1  13000  faclbnd  13077  faclbnd4lem1  13080  facubnd  13087  seqcoll  13248  sqrlem7  13989  absle  14055  releabs  14061  absrdbnd  14081  rexuzre  14092  limsupgre  14212  lo1bddrp  14256  rlimclim1  14276  rlimresb  14296  rlimrege0  14310  o1add  14344  o1sub  14346  climsqz  14371  climsqz2  14372  rlimsqzlem  14379  rlimsqz  14380  rlimsqz2  14381  rlimno1  14384  isercoll  14398  caucvgrlem  14403  iseraltlem3  14414  o1fsum  14545  cvgcmp  14548  cvgcmpce  14550  climcnds  14583  expcnv  14596  cvgrat  14615  mertenslem2  14617  fprodle  14727  eftlub  14839  rpnnen2lem12  14954  bitsfzo  15157  isprm5  15419  isprm7  15420  eulerthlem2  15487  pcmpt2  15597  pcfac  15603  prmreclem3  15622  prmreclem4  15623  prmreclem5  15624  4sqlem11  15659  vdwlem1  15685  vdwlem3  15687  setsstruct2  15896  prdsxmetlem  22173  nrmmetd  22379  nm2dif  22429  nlmvscnlem2  22489  nmoco  22541  nmotri  22543  nghmcn  22549  icccmplem2  22626  reconnlem2  22630  elii1  22734  xrhmeo  22745  cnheiborlem  22753  bndth  22757  tchcphlem1  23034  ipcnlem2  23043  cncmet  23119  trirn  23183  minveclem2  23197  minveclem4  23203  ivthlem2  23221  ovolunlem1a  23264  ovolunlem1  23265  ovolfiniun  23269  ovoliunlem1  23270  ovolicc2lem4  23288  ovolicc2lem5  23289  ovolicopnf  23292  nulmbl2  23304  ioombl1lem4  23329  ioorcl2  23340  uniioombllem3  23353  uniioombllem4  23354  uniioombllem5  23355  volcn  23374  vitalilem2  23378  vitali  23382  mbfi1fseqlem5  23486  mbfi1fseqlem6  23487  itg2splitlem  23515  itg2monolem1  23517  itg2monolem3  23519  itg2mono  23520  itg2cnlem1  23528  itgle  23576  bddmulibl  23605  ditgsplitlem  23624  dveflem  23742  dvlip  23756  dveq0  23763  dvfsumabs  23786  dvfsumlem1  23789  dvfsumlem2  23790  dvfsumlem3  23791  dvfsumlem4  23792  dvfsum2  23797  fta1glem2  23926  dgradd2  24024  plydiveu  24053  fta1lem  24062  aalioulem2  24088  aalioulem3  24089  aalioulem4  24090  aalioulem5  24091  aaliou3lem8  24100  aaliou3lem9  24105  ulmbdd  24152  ulmcn  24153  mtest  24158  mtestbdd  24159  abelthlem2  24186  abelthlem7  24192  pilem2  24206  tanabsge  24258  cosordlem  24277  tanord  24284  logneg2  24361  abslogle  24364  dvlog2lem  24398  cxple2a  24445  abscxpbnd  24494  atans2  24658  leibpi  24669  o1cxp  24701  cxploglim2  24705  jensenlem2  24714  emcllem6  24727  harmoniclbnd  24735  harmonicubnd  24736  harmonicbnd4  24737  fsumharmonic  24738  lgamgulmlem2  24756  lgamgulmlem3  24757  lgamgulmlem5  24759  lgambdd  24763  ftalem2  24800  basellem3  24809  basellem5  24811  basellem6  24812  dvdsflsumcom  24914  fsumfldivdiaglem  24915  ppiub  24929  chtublem  24936  logfac2  24942  chpub  24945  logfacubnd  24946  logfaclbnd  24947  logfacbnd3  24948  logexprlim  24950  bcmono  25002  bpos1lem  25007  bposlem1  25009  bposlem2  25010  bposlem3  25011  bposlem4  25012  bposlem5  25013  bposlem6  25014  bposlem7  25015  bposlem9  25017  lgsdirprm  25056  lgsquadlem1  25105  2lgslem1c  25118  2sqlem8  25151  chebbnd1lem1  25158  chebbnd1lem3  25160  chtppilimlem1  25162  chpchtlim  25168  vmadivsumb  25172  rplogsumlem1  25173  rplogsumlem2  25174  rpvmasumlem  25176  dchrisumlema  25177  dchrisumlem2  25179  dchrisumlem3  25180  dchrmusum2  25183  dchrvmasumlem2  25187  dchrvmasumlem3  25188  dchrvmasumlema  25189  dchrvmasumiflem1  25190  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0fno1  25200  dchrisum0re  25202  dchrisum0lem1b  25204  dchrisum0lem1  25205  dchrisum0lem2a  25206  dchrisum0  25209  rplogsum  25216  mudivsum  25219  mulogsumlem  25220  logdivsum  25222  mulog2sumlem1  25223  mulog2sumlem2  25224  2vmadivsumlem  25229  log2sumbnd  25233  selberglem2  25235  selbergb  25238  selberg2lem  25239  selberg2b  25241  chpdifbndlem1  25242  logdivbnd  25245  selberg3lem1  25246  selberg3lem2  25247  selberg4lem1  25249  pntrmax  25253  pntrsumo1  25254  pntrsumbnd  25255  pntrlog2bndlem1  25266  pntrlog2bndlem2  25267  pntrlog2bndlem3  25268  pntrlog2bndlem5  25270  pntrlog2bndlem6  25272  pntrlog2bnd  25273  pntpbnd1a  25274  pntpbnd1  25275  pntpbnd2  25276  pntibndlem2  25280  pntibndlem3  25281  pntlemg  25287  pntlemr  25291  pntlemj  25292  pntlemf  25294  pntlemk  25295  pntlemo  25296  pntleml  25300  abvcxp  25304  qabvle  25314  padicabv  25319  ostth2lem2  25323  ostth2lem3  25324  ostth3  25327  axlowdimlem16  25837  axcontlem8  25851  axcontlem10  25853  wwlksm1edg  26767  wwlksubclwwlks  26925  smcnlem  27552  nmoub3i  27628  ubthlem3  27728  minvecolem2  27731  minvecolem3  27732  minvecolem4  27736  htthlem  27774  bcs2  28039  pjhthlem1  28250  cnlnadjlem2  28927  cnlnadjlem7  28932  nmopadjlem  28948  nmoptrii  28953  nmopcoadji  28960  leopnmid  28997  cdj1i  29292  nndiffz1  29548  pmtrto1cl  29849  psgnfzto1stlem  29850  fzto1st  29853  psgnfzto1st  29855  smatrcl  29862  submateqlem1  29873  nexple  30071  esumpcvgval  30140  oddpwdc  30416  eulerpartlems  30422  eulerpartlemgc  30424  eulerpartlemb  30430  dstfrvunirn  30536  orvclteinc  30537  ballotlemsima  30577  ballotlemfrcn0  30591  signstfveq0  30654  fsum2dsub  30685  breprexplemc  30710  breprexp  30711  logdivsqrle  30728  hgt750lemb  30734  hgt750leme  30736  tgoldbachgnn  30737  dnibndlem2  32469  dnibndlem6  32473  dnibndlem9  32476  dnibndlem10  32477  dnibndlem11  32478  dnibndlem12  32479  knoppcnlem4  32486  unblimceq0lem  32497  unblimceq0  32498  unbdqndv2lem2  32501  knoppndvlem11  32513  knoppndvlem14  32516  knoppndvlem15  32517  knoppndvlem18  32520  knoppndvlem21  32523  poimirlem6  33415  poimirlem7  33416  poimirlem13  33422  poimirlem15  33424  poimirlem29  33438  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  itg2addnc  33464  iblmulc2nc  33475  bddiblnc  33480  ftc1anclem7  33491  ftc1anclem8  33492  filbcmb  33535  geomcau  33555  prdsbnd  33592  cntotbnd  33595  bfplem2  33622  rrntotbnd  33635  iccbnd  33639  lzunuz  37331  irrapxlem3  37388  irrapxlem4  37389  irrapxlem5  37390  pellexlem2  37394  pell1qrge1  37434  monotoddzzfi  37507  jm2.17a  37527  rmygeid  37531  fzmaxdif  37548  jm2.27c  37574  jm3.1lem1  37584  expdiophlem1  37588  imo72b2lem0  38465  int-ineqtransd  38497  dvgrat  38511  monoords  39511  absnpncan2d  39516  absnpncan3d  39521  ssfiunibd  39523  leadd12dd  39532  rexabslelem  39645  uzublem  39657  sqrlearg  39780  fmul01  39812  fmul01lt1lem1  39816  fmul01lt1lem2  39817  climsuselem1  39839  climsuse  39840  limsupresico  39932  limsupubuzlem  39944  limsupmnfuzlem  39958  limsupre3uzlem  39967  liminfresico  40003  limsup10exlem  40004  cnrefiisplem  40055  dvdivbd  40138  dvbdfbdioolem2  40144  ioodvbdlimc1lem1  40146  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  iblspltprt  40189  itgspltprt  40195  stoweidlem1  40218  stoweidlem3  40220  stoweidlem5  40222  stoweidlem11  40228  stoweidlem17  40234  stoweidlem20  40237  stoweidlem26  40243  stoweidlem34  40251  wallispilem4  40285  stirlinglem11  40301  stirlinglem12  40302  stirlinglem13  40303  fourierdlem12  40336  fourierdlem15  40339  fourierdlem20  40344  fourierdlem30  40354  fourierdlem39  40363  fourierdlem42  40366  fourierdlem47  40370  fourierdlem50  40373  fourierdlem64  40387  fourierdlem65  40388  fourierdlem68  40391  fourierdlem73  40396  fourierdlem77  40400  fourierdlem79  40402  fourierdlem87  40410  elaa2lem  40450  etransclem23  40474  ioorrnopnlem  40524  salgencntex  40561  sge0le  40624  sge0isum  40644  sge0xaddlem1  40650  hoicvr  40762  hsphoidmvle2  40799  hoidmv1lelem1  40805  hoidmv1lelem2  40806  hoidmv1lelem3  40807  hoidmvlelem1  40809  hoidmvlelem2  40810  hoidmvlelem4  40812  hspmbllem1  40840  hspmbllem2  40841  smfmullem1  40998  smfmullem2  40999  smfmullem3  41000  smfsuplem1  41017  lighneallem4a  41525  fllog2  42362