Theorem lelttr 9692

Description: Transitive law. (Contributed by NM, 23-May-1999.)

Assertion

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

Proof of Theorem lelttr

Step	Hyp	Ref	Expression
1		leloe 9688	. . . 4 |- ( ( A e. RR /\ B e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
2	1	3adant3 1016	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B <-> ( A < B \/ A = B ) ) )
3		lttr 9678	. . . . 5 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B < C ) -> A < C ) )
4	3	expd 436	. . . 4 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( B < C -> A < C ) ) )
5		breq1 4459	. . . . . 6 |- ( A = B -> ( A < C <-> B < C ) )
6	5	biimprd 223	. . . . 5 |- ( A = B -> ( B < C -> A < C ) )
7	6	a1i 11	. . . 4 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A = B -> ( B < C -> A < C ) ) )
8	4, 7	jaod 380	. . 3 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B \/ A = B ) -> ( B < C -> A < C ) ) )
9	2, 8	sylbid 215	. 2 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A <_ B -> ( B < C -> A < C ) ) )
10	9	impd 431	1 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A <_ B /\ B < C ) -> A < C ) )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 973   = wceq 1395   e. wcel 1819   class class class wbr 4456   RRcr 9508   < clt 9645   <_ cle 9646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-resscn 9566  ax-pre-lttri 9583  ax-pre-lttrn 9584

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-er 7329  df-en 7536  df-dom 7537  df-sdom 7538  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651

This theorem is referenced by:  letr  9695  lelttri  9728  lelttrd  9757  letrp1  10405  ltmul12a  10419  ledivp1  10467  supmul1  10528  bndndx  10815  uzind  10975  fnn0ind  10984  rpnnen1lem5  11237  xrinfmsslem  11524  elfzo0z  11864  fzofzim  11868  elfzodifsumelfzo  11885  flge  11945  flflp1  11947  flltdivnn0lt  11968  fsequb  12088  expnlbnd2  12300  ccat2s1fvw  12651  swrdswrd  12697  swrdccatin12lem3  12727  repswswrd  12768  caubnd2  13202  caubnd  13203  mulcn2  13430  cn1lem  13432  rlimo1  13451  o1rlimmul  13453  climsqz  13475  climsqz2  13476  rlimsqzlem  13483  climsup  13504  caucvgrlem2  13509  iseralt  13519  cvgcmp  13642  cvgcmpce  13644  ruclem3  13978  ruclem12  13986  algcvgblem  14218  pclem  14374  infpn2  14443  gsummoncoe1  18473  mp2pm2mplem4  19437  metss2lem  21140  ngptgp  21276  nghmcn  21378  iocopnst  21566  ovollb2lem  22025  ovolicc2lem4  22057  volcn  22141  ismbf3d  22187  dvcnvrelem1  22544  dvfsumrlim  22558  ulmcn  22920  mtest  22925  logdivlti  23131  isosctrlem1  23278  ftalem2  23473  chtub  23613  bposlem6  23690  chtppilim  23786  dchrisumlem3  23802  pntlem3  23920  nvnencycllem  24770  clwlkisclwwlklem2a  24912  vacn  25731  nmcvcn  25732  blocni  25847  chscllem2  26683  lnconi  27079  staddi  27292  stadd3i  27294  ltflcei  30248  geomcau  30457  heibor1lem  30510  bfplem2  30524  rrncmslem  30533  climinf  31815  leltletr  32582  zm1nn  32589  el2fzo  32603  ply1mulgsumlem2  33131