Theorem ltletrt 5537

Description: Transitive law.

Assertion

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

Proof of Theorem ltletrt

Step	Hyp	Ref	Expression
1		leloet 5531	. . . . 5 |- ((B e. RR /\ C e. RR) -> (B <_ C <-> (B < C \/ B = C)))
2	1	3adant1 801	. . . 4 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (B <_ C <-> (B < C \/ B = C)))
3		axlttrn 5517	. . . . . . 7 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) -> A < C))
4	3	exp3a 376	. . . . . 6 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B -> (B < C -> A < C)))
5	4	com23 32	. . . . 5 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (B < C -> (A < B -> A < C)))
6		breq2 2636	. . . . . . 7 |- (B = C -> (A < B <-> A < C))
7	6	biimpd 153	. . . . . 6 |- (B = C -> (A < B -> A < C))
8	7	a1i 8	. . . . 5 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (B = C -> (A < B -> A < C)))
9	5, 8	jaod 426	. . . 4 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((B < C \/ B = C) -> (A < B -> A < C)))
10	2, 9	sylbid 203	. . 3 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (B <_ C -> (A < B -> A < C)))
11	10	com23 32	. 2 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B -> (B <_ C -> A < C)))
12	11	imp3a 361	1 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B <_ C) -> A < C))

Syntax hints:   -> wi 3   <-> wb 146   \/ wo 222   /\ wa 223   /\ w3a 779   = wceq 960   e. wcel 962   class class class wbr 2632  RRcr 5246   <_ cle 5308   < clt 5499

This theorem is referenced by:  ltletrd 5541  ltletr 5600  ltleaddt 5658  lediv12it 5902  nngt0t 5952  nnrecgt0t 5959  nnaddm1clt 5964  xrsupsslem 6082  uzwo3lem1 6225  zbtwnre 6230  ceilet 6259  qbtwnre 6289  icounlem 6362  ioojoint 6366  fsequb 6473  seq1bnd 6924  caubnd 6940  caucvglem6 7176  expcnvlem1 7241  ivthlem7 7301  efaddlem23 7374  cos01gt0 7492  znnenlem 7516  ssbl 7864  lmnn 7944

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1129  ax-10o 1146  ax-16 1216  ax-11o 1224  ax-ext 1466  ax-rep 2706  ax-sep 2716  ax-nul 2723  ax-pow 2756  ax-pr 2793  ax-un 2880  ax-inf2 4637

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1178  df-eu 1388  df-mo 1389  df-clab 1471  df-cleq 1476  df-clel 1479  df-ne 1594  df-nel 1595  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2010  df-dif 2058  df-un 2059  df-in 2060  df-ss 2062  df-pss 2064  df-nul 2290  df-if 2372  df-pw 2412  df-sn 2422  df-pr 2423  df-tp 2425  df-op 2426  df-uni 2516  df-int 2546  df-iun 2580  df-br 2633  df-opab 2680  df-tr 2694  df-eprel 2846  df-id 2849  df-po 2854  df-so 2864  df-fr 2931  df-we 2948  df-ord 2965  df-on 2966  df-lim 2967  df-suc 2968  df-om 3146  df-xp 3198  df-rel 3199  df-cnv 3200  df-co 3201  df-dm 3202  df-rn 3203  df-res 3204  df-ima 3205  df-fun 3206  df-fn 3207  df-f 3208  df-f1 3209  df-fo 3210  df-f1o 3211  df-fv 3212  df-rdg 3946  df-opr 3979  df-oprab 3980  df-1st 4093  df-2nd 4094  df-1o 4147  df-oadd 4149  df-omul 4150  df-er 4275  df-ec 4277  df-qs 4280  df-en 4382  df-dom 4383  df-sdom 4384  df-ni 5013  df-pli 5014  df-mi 5015  df-lti 5016  df-plpq 5048  df-mpq 5049  df-enq 5050  df-nq 5051  df-plq 5052  df-mq 5053  df-rq 5054  df-ltq 5055  df-1q 5056  df-np 5099  df-1p 5100  df-plp 5101  df-ltp 5103  df-enr 5179  df-nr 5180  df-ltr 5183  df-0r 5184  df-c 5253  df-r 5257  df-lt 5260  df-pnf 5500  df-mnf 5501  df-xr 5502  df-ltxr 5503  df-le 5504

Copyright terms: Public domain