Theorem letr 10131

Description: Transitive law. (Contributed by NM, 12-Nov-1999.)

Assertion

Ref	Expression
letr	|- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		leloe 10124	. . . . 5 |- ( ( B e. RR /\ C e. RR ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
2	1	3adant1 1079	. . . 4 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
3	2	adantr 481	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( B <_ C <-> ( B < C \/ B = C ) ) )
4		lelttr 10128	. . . . . 6 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A < C ) )
5		ltle 10126	. . . . . . 7 |- ( ( A e. RR /\ C e. RR ) -> ( A < C -> A <_ C ) )
6	5	3adant2 1080	. . . . . 6 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < C -> A <_ C ) )
7	4, 6	syld 47	. . . . 5 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A <_ C ) )
8	7	expdimp 453	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( B < C -> A <_ C ) )
9		breq2 4657	. . . . . 6 |- ( B = C -> ( A <_ B <-> A <_ C ) )
10	9	biimpcd 239	. . . . 5 |- ( A <_ B -> ( B = C -> A <_ C ) )
11	10	adantl 482	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( B = C -> A <_ C ) )
12	8, 11	jaod 395	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( ( B < C \/ B = C ) -> A <_ C ) )
13	3, 12	sylbid 230	. 2 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ A <_ B ) -> ( B <_ C -> A <_ C ) )
14	13	expimpd 629	1 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B <_ C ) -> A <_ C ) )

Syntax hints:   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   class class class wbr 4653   RRcr 9935   < clt 10074   <_ 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:  letri  10166  letrd  10194  le2add  10510  le2sub  10527  p1le  10866  lemul12b  10880  lemul12a  10881  zletr  11421  peano2uz2  11465  ledivge1le  11901  lemaxle  12026  elfz1b  12409  elfz0fzfz0  12444  fz0fzelfz0  12445  fz0fzdiffz0  12448  elfzmlbp  12450  difelfznle  12453  elincfzoext  12525  ssfzoulel  12562  ssfzo12bi  12563  flge  12606  flflp1  12608  fldiv4p1lem1div2  12636  fldiv4lem1div2uz2  12637  monoord  12831  leexp2r  12918  expubnd  12921  le2sq2  12939  facwordi  13076  faclbnd3  13079  facavg  13088  fi1uzind  13279  fi1uzindOLD  13285  swrdswrdlem  13459  swrdccat  13493  sqrlem1  13983  sqrlem6  13988  sqrlem7  13989  leabs  14039  limsupbnd2  14214  rlim3  14229  lo1bdd2  14255  lo1bddrp  14256  o1lo1  14268  lo1mul  14358  lo1le  14382  isercolllem2  14396  iseraltlem2  14413  fsumabs  14533  cvgrat  14615  ruclem9  14967  algcvga  15292  prmdvdsfz  15417  prmfac1  15431  eulerthlem2  15487  modprm0  15510  prmreclem1  15620  prmreclem4  15623  4sqlem11  15659  vdwnnlem3  15701  gsumbagdiaglem  19375  zntoslem  19905  cnllycmp  22755  evth  22758  ovoliunlem2  23271  ovolicc2lem3  23287  itg2monolem1  23517  coeaddlem  24005  coemullem  24006  aalioulem5  24091  aalioulem6  24092  sincosq1lem  24249  emcllem6  24727  ftalem3  24801  fsumvma2  24939  chpchtsum  24944  bcmono  25002  bposlem5  25013  gausslemma2dlem1a  25090  lgsquadlem1  25105  dchrisum0lem1  25205  pntrsumbnd2  25256  pntleml  25300  brbtwn2  25785  axlowdimlem17  25838  axlowdim  25841  crctcshwlkn0lem3  26704  crctcshwlkn0lem5  26706  wwlksubclwwlks  26925  clwlksfclwwlk  26962  eupth2lems  27098  nmoub3i  27628  ubthlem1  27726  ubthlem2  27727  nmopub2tALT  28768  nmfnleub2  28785  lnconi  28892  leoptr  28996  pjnmopi  29007  cdj3lem2b  29296  eulerpartlemb  30430  isbasisrelowllem1  33203  isbasisrelowllem2  33204  ltflcei  33397  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  bddiblnc  33480  dvasin  33496  incsequz  33544  mettrifi  33553  equivbnd  33589  bfplem1  33621  jm2.17b  37528  fmul01lt1lem2  39817  eluzge0nn0  41322  elfz2z  41325  iccpartiltu  41358  iccpartgt  41363  lighneallem2  41523