Theorem leo 158

Description: L.e. absorption.

Assertion

Ref	Expression
leo	a ≤ (a ∪ b)

Proof of Theorem leo

Step	Hyp	Ref	Expression
1		a5c 121	. 2 (a ∩ (a ∪ b)) = a
2	1	df2le1 135	1 a ≤ (a ∪ b)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem is referenced by:  leor 159  leao1 162  leao2 163  ledio 176  comorr 184  distlem 188  womao 220  womaon 221  womaa 222  womaan 223  anorabs2 224  ka4lemo 228  bina3 284  bina4 285  nom14 311  nom21 314  nom22 315  nom24 317  i1or 345  i5lei4 350  k1-8a 355  2vwomlem 365  wr5-2v 366  ska2 432  gsth 489  i3bi 496  df2i3 498  dfi3b 499  oi3ai3 503  i3th8 550  i3con 551  i3orlem2 553  i3orlem4 555  i3orlem5 556  i3orlem7 558  ud3lem1a 566  ud3lem3d 575  ud3lem3 576  ud4lem1a 577  ud4lem1b 578  ud4lem1c 579  ud5lem1b 587  ud5lem1 589  u4lemana 608  u4lemona 628  u3lemob 632  u1lemc6 706  comi12 707  i2bi 722  u12lembi 726  u4lem1 737  u4lem6 768  u12lem 771  u1lem8 776  u1lem9b 778  u3lem13b 790  bi1o1a 798  test2 803  3vth6 809  3vded11 814  3vded12 815  2oalem1 825  mlalem 832  sadm3 838  bi3 839  orbi 842  negantlem1 848  negantlem2 849  negantlem3 850  negantlem9 859  neg3antlem1 864  neg3antlem2 865  comanb 872  mhlemlem1 874  mhlem 876  mh 879  cancellem 891  e2astlem1 895  gomaex3h3 904  gomaex3lem10 923  oas 925  oatr 928  oau 929  oa23 936  oa4lem1 937  distoah2 941  distoah4 943  oa3to4lem1 945  oa6to4h1 955  oa6to4h2 956  oa6to4h3 957  oa4to6lem1 960  oa4btoc 966  oa3-6lem 980  oa3-u1lem 985  oa3-2to2s 990  d3oa 995  d4oa 996  oaliv 1003  oadist2a 1007  mloa 1018  oadistd 1023  axoa4a 1036  4oadist 1043  lem3.3.5 1054  lem3.3.7i4e1 1068  lem4.6.6i0j1 1085  lem4.6.6i0j2 1086  lem4.6.6i0j3 1087  lem4.6.6i0j4 1088  lem4.6.6i1j3 1091  lem4.6.6i2j1 1093  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j2 1098

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

Copyright terms: Public domain