Theorem letr 137

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 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		a5c 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 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  ska2 432  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 1033  4oadist 1043  lem3.3.5 1054

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

Copyright terms: Public domain