Theorem ltletr 7979

Description: Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.)

Assertion

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

Proof of Theorem ltletr

Step	Hyp	Ref	Expression
1		simprr 522	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> B <_ C )
2		simpl2 990	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> B e. RR )
3		simpl3 991	. . . . 5 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> C e. RR )
4		lenlt 7965	. . . . 5 |- ( ( B e. RR /\ C e. RR ) -> ( B <_ C <-> -. C < B ) )
5	2, 3, 4	syl2anc 409	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> ( B <_ C <-> -. C < B ) )
6	1, 5	mpbid 146	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> -. C < B )
7		simprl 521	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> A < B )
8		axltwlin 7957	. . . . 5 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( A < B -> ( A < C \/ C < B ) ) )
9	8	adantr 274	. . . 4 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> ( A < B -> ( A < C \/ C < B ) ) )
10	7, 9	mpd 13	. . 3 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> ( A < C \/ C < B ) )
11	6, 10	ecased 1338	. 2 |- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A < B /\ B <_ C ) ) -> A < C )
12	11	ex 114	1 |- ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( A < B /\ B <_ C ) -> A < C ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 103   <-> wb 104   \/ wo 698   /\ w3a 967   e. wcel 2135   class class class wbr 3976   RRcr 7743   < clt 7924   <_ cle 7925

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-13 2137  ax-14 2138  ax-ext 2146  ax-sep 4094  ax-pow 4147  ax-pr 4181  ax-un 4405  ax-setind 4508  ax-cnex 7835  ax-resscn 7836  ax-pre-ltwlin 7857

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-fal 1348  df-nf 1448  df-sb 1750  df-eu 2016  df-mo 2017  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ne 2335  df-nel 2430  df-ral 2447  df-rex 2448  df-rab 2451  df-v 2723  df-dif 3113  df-un 3115  df-in 3117  df-ss 3124  df-pw 3555  df-sn 3576  df-pr 3577  df-op 3579  df-uni 3784  df-br 3977  df-opab 4038  df-xp 4604  df-cnv 4606  df-pnf 7926  df-mnf 7927  df-xr 7928  df-ltxr 7929  df-le 7930

This theorem is referenced by:  ltletri  7996  ltletrd  8312  ltleadd  8335  nngt0  8873  nnrecgt0  8886  elnnnn0c  9150  elnnz1  9205  zltp1le  9236  uz3m2nn  9502  ledivge1le  9653  addlelt  9695  zltaddlt1le  9934  elfz1b  10015  elfzodifsumelfzo  10126  ssfzo12bi  10150  cos01gt0  11689  oddge22np1  11803  nn0seqcvgd  11952  coprm  12053  logdivlti  13343