Theorem lbtr 139

Description: Transitive inference. (Contributed by NM, 28-Aug-1997.)

Hypotheses

Ref	Expression
lbtr.1	a ≤ b
lbtr.2	b = c

Assertion

Ref	Expression
lbtr	a ≤ c

Proof of Theorem lbtr

Step	Hyp	Ref	Expression
1		lbtr.2	. . . . 5 b = c
2	1	ax-r1 35	. . . 4 c = b
3	2	lan 77	. . 3 (a ∩ c) = (a ∩ b)
4		lbtr.1	. . . 4 a ≤ b
5	4	df2le2 136	. . 3 (a ∩ b) = a
6	3, 5	ax-r2 36	. 2 (a ∩ c) = a
7	6	df2le1 135	1 a ≤ c

Syntax hints:   = wb 1   ≤ wle 2   ∩ wa 7

This theorem was proved from axioms:  ax-a1 30  ax-a2 31  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:  le3tr1  140  lerr  150  lecon2  156  leor  159  lel2or  170  lel2an  171  ledi  174  ledio  176  ka4lemo  228  wlem1  243  ska15  244  bina4  285  bina5  286  womle2b  296  womle3b  297  nom14  311  nom20  313  nom23  316  nom24  317  go1  343  i2or  344  i1or  345  k1-8a  355  k1-8b  356  wom2  434  ka4ot  435  ortha  438  i3bi  496  lem4  511  binr3  519  i3th5  547  i3th7  549  i3th8  550  i3orlem1  552  i3orlem4  555  i3orlem7  558  i3orlem8  559  ud3lem1c  568  ud4lem1c  579  u1lemc6  706  i2bi  722  u12lembi  726  u1lem9b  778  u3lem14mp  794  3vth6  809  3vded11  814  3vded12  815  3vded21  817  3vded22  818  oaeqv  830  sadm3  838  bi3  839  bi4  840  mlaconj4  844  mlaconj  845  negantlem1  848  negantlem2  849  negantlem3  850  negantlem9  859  negantlem10  861  neg3antlem1  864  neg3antlem2  865  neg3ant1  866  elimconslem  867  elimcons  868  mhlem  876  mhlem2  878  marsdenlem3  882  marsdenlem4  883  mlaconjolem  885  mlaconjo  886  mhcor1  888  oago3.29  889  oago3.21x  890  cancellem  891  kb10iii  893  e2ast2  894  govar2  897  gomaex4  900  gomaex3h3  904  gomaex3h6  907  gomaex3h7  908  gomaex3h8  909  gomaex3lem4  917  oas  925  oat  927  oatr  928  oau  929  oaur  930  oal42  935  oa23  936  oa4lem1  937  oa4lem2  938  oa3to4lem1  945  oa3to4lem2  946  oa6to4h1  955  oa6to4h2  956  oa6to4h3  957  oa4to6lem1  960  oa4to6lem2  961  oa4to6lem3  962  oa4btoc  966  oa3-u2lem  986  oa3-2to2s  990  oa3-1to5  993  d3oa  995  d4oa  996  oaliv  1003  oalem1  1005  oadist2a  1007  oadist2b  1008  oagen1  1014  oagen2  1016  mloa  1018  oadistc0  1021  oadistc  1022  oadistd  1023  oa4cl  1027  oa3moa3  1029  axoa4a  1037  4oagen1  1042  4oadist  1044  lem3.3.5  1055  lem3.4.3  1076  lem4.6.7  1103  ml3le  1129  vneulem7  1137  vneulemexp  1148  l42mod  1151  dp15lema  1154  dp15leme  1158  dp15lemf  1159  dp15lemh  1161  dp53lema  1163  dp53lemc  1165  dp53lemd  1166  dp53lemf  1168  dp35lemd  1174  dp35lemc  1175  dp35lembb  1177  dp35lem0  1179  dp34  1181  dp41leml  1193  dp41lemm  1194  dp32  1196  xdp41  1198  xdp15  1199  xdp53  1200  xxdp41  1201  xxdp15  1202  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemc  1211