Theorem letr 129

Description: Transitive law for l.e.

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 123	. . . . . . 7 (a v b) = b
3	2	ax-r5 37	. . . . . 6 ((a v b) v c) = (b v c)
4	3	ax-r1 34	. . . . 5 (b v c) = ((a v b) v c)
5		letr.2	. . . . . 6 b =< c
6	5	df-le2 123	. . . . 5 (b v c) = c
7		ax-a3 31	. . . . 5 ((a v b) v c) = (a v (b v c))
8	4, 6, 7	3tr2 61	. . . 4 c = (a v (b v c))
9	8	lan 70	. . 3 (a ^ c) = (a ^ (a v (b v c)))
10		a5c 113	. . 3 (a ^ (a v (b v c))) = a
11	9, 10	ax-r2 35	. 2 (a ^ c) = a
12	11	df2le1 127	1 a =< c

Syntax hints:   =< wle 2   v wo 6   ^ wa 7

This theorem is referenced by:  leao1 154  leao2 155  leao3 156  leao4 157  le2or 160  le2an 161  distlem 180  str 181  womao 212  womaon 213  womaa 214  womaan 215  anorabs2 216  anorabs 217  ka4lemo 220  ska13 233  womle 290  nom20 305  nom21 306  nom22 307  wom3 349  ska2 414  gsth 471  i3bi 478  df2i3 480  dfi3b 481  oi3ai3 485  binr2 500  i3con 533  i3orlem2 535  i3orlem3 536  i3orlem7 540  ud3lem1a 548  ud3lem1c 550  ud3lem1d 551  ud3lem3a 554  ud3lem3d 557  ud3lem3 558  ud4lem1b 560  ud4lem1c 561  ud4lem1 563  ud5lem1b 569  ud5lem1 571  u4lemona 610  u1lemob 612  u3lemob 614  u5lemob 616  u1lemc6 688  comi12 689  u12lembi 708  u4lem1 719  u4lem2 729  u4lem6 750  u1lem8 758  u1lem9ab 761  u3lem13b 772  u3lem14mp 776  bi1o1a 780  test2 785  3vth1 786  3vded12 797  3vded22 800  1oa 802  2oalem1 807  oale 811  oaeqv 812  mlalem 814  eqtr4 816  sa5 818  sadm3 820  bi3 821  imp3 823  orbi 824  mlaconj4 826  mlaconj2 828  negantlem2 831  negantlem3 832  negantlem9 841  negantlem10 843  neg3antlem1 846  neg3antlem2 847  elimconslem 849  elimcons 850  comanblem1 852  comanb 854  mhlemlem1 856  mhlem 858  mh 861  mlaconjo 868  oago3.21x 872  cancellem 873  kb10iii 875  gon2n 878  gomaex3lem10 903  oas 905  oasr 906  oat 907  oatr 908  oaur 910  oaidlem2 911  oaidlem2g 912  oal42 915  oa4lem3 919  oa3to4lem1 925  oa3to4lem2 926  oa3to4lem4 928  oa4b 939  oa4to6lem1 940  oa4to6lem2 941  oa4to6lem3 942  oa4to6dual 944  oa4btoc 946  oa4to4u2 954  oa4uto4g 955  oa4uto4 957  oa3-u1lem 965  oa3-u1 971  oa3-1to5 973  d3oa 975  d4oa 976  oaliv 983  oadist2a 987  oacom2 992  oagen2 996  oagen2b 997  mloa 998  oadist 999  oadistc0 1001  oadistc 1002  oadistd 1003  axoa4 1013  4oadist 1023

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

This theorem depends on definitions:  df-a 39  df-le1 122  df-le2 123

metamath.org