Theorem letr 137

Description: Transitive law for "less than or equal to". (Contributed by NM, 27-Aug-1997.)

Hypotheses

Ref	Expression
letr.1	a ≤ b
letr.2	b ≤ c

Assertion

Ref	Expression
letr	a ≤ c

Proof of Theorem letr

Step	Hyp	Ref	Expression
1		letr.1	. . . . . . . 8 a ≤ b
2	1	df-le2 131	. . . . . . 7 (a ∪ b) = b
3	2	ax-r5 38	. . . . . 6 ((a ∪ b) ∪ c) = (b ∪ c)
4	3	ax-r1 35	. . . . 5 (b ∪ c) = ((a ∪ b) ∪ c)
5		letr.2	. . . . . 6 b ≤ c
6	5	df-le2 131	. . . . 5 (b ∪ c) = c
7		ax-a3 32	. . . . 5 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
8	4, 6, 7	3tr2 64	. . . 4 c = (a ∪ (b ∪ c))
9	8	lan 77	. . 3 (a ∩ c) = (a ∩ (a ∪ (b ∪ c)))
10		anabs 121	. . 3 (a ∩ (a ∪ (b ∪ c))) = a
11	9, 10	ax-r2 36	. 2 (a ∩ c) = a
12	11	df2le1 135	1 a ≤ c

Syntax hints:   ≤ wle 2   ∪ wo 6   ∩ wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  ax-a3 32  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This theorem depends on definitions:  df-a 40  df-le1 130  df-le2 131

This theorem is referenced by:  leao1  162  leao2  163  leao3  164  leao4  165  le2or  168  le2an  169  distlem  188  str  189  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  ka4lemo  228  ska13  241  womle  298  nom20  313  nom21  314  nom22  315  wom3  367  gsth  489  i3bi  496  df2i3  498  dfi3b  499  oi3ai3  503  binr2  518  i3con  551  i3orlem2  553  i3orlem3  554  i3orlem7  558  ud3lem1a  566  ud3lem1c  568  ud3lem1d  569  ud3lem3a  572  ud3lem3d  575  ud3lem3  576  ud4lem1b  578  ud4lem1c  579  ud4lem1  581  ud5lem1b  587  ud5lem1  589  u4lemona  628  u1lemob  630  u3lemob  632  u5lemob  634  u1lemc6  706  comi12  707  u12lembi  726  u4lem1  737  u4lem2  747  u4lem6  768  u1lem8  776  u1lem9ab  779  u3lem13b  790  u3lem14mp  794  bi1o1a  798  test2  803  3vth1  804  3vded12  815  3vded22  818  1oa  820  2oalem1  825  oale  829  oaeqv  830  mlalem  832  eqtr4  834  sa5  836  sadm3  838  bi3  839  imp3  841  orbi  842  mlaconj4  844  mlaconj2  846  negantlem2  849  negantlem3  850  negantlem9  859  negantlem10  861  neg3antlem1  864  neg3antlem2  865  elimconslem  867  elimcons  868  comanblem1  870  comanb  872  mhlemlem1  874  mhlem  876  mh  879  mlaconjo  886  oago3.21x  890  cancellem  891  kb10iii  893  gon2n  898  gomaex3lem10  923  oas  925  oasr  926  oat  927  oatr  928  oaur  930  oaidlem2  931  oaidlem2g  932  oal42  935  oa4lem3  939  oa3to4lem1  945  oa3to4lem2  946  oa3to4lem4  948  oa4b  959  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4to6dual  964  oa4btoc  966  oa4to4u2  974  oa4uto4g  975  oa4uto4  977  oa3-u1lem  985  oa3-u1  991  oa3-1to5  993  d3oa  995  d4oa  996  oaliv  1003  oadist2a  1007  oacom2  1012  oagen2  1016  oagen2b  1017  mloa  1018  oadist  1019  oadistc0  1021  oadistc  1022  oadistd  1023  axoa4  1034  4oadist  1044  lem3.3.5  1055  dp15lema  1154  dp15lemh  1161  dp53lema  1163  dp53lemd  1166  dp53leme  1167  dp53lemf  1168  dp53lemg  1169  dp35leme  1173  dp35lemd  1174  dp35lema  1178  dp35lem0  1179  dp34  1181  dp41lemh  1190  dp41lemm  1194  dp23  1197  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208