Theorem leor 159

Description: L.e. absorption.

Assertion

Ref	Expression
leor	a =< (b v a)

Proof of Theorem leor

Step	Hyp	Ref	Expression
1		leo 158	. 2 a =< (a v b)
2		ax-a2 31	. 2 (a v b) = (b v a)
3	1, 2	lbtr 139	1 a =< (b v a)

Syntax hints:   =< wle 2   v wo 6

This theorem is referenced by:  leao3 164  leao4 165  womao 220  womaon 221  womaa 222  womaan 223  anorabs2 224  womle 298  nom20 313  i1or 345  i5lei3 349  ska2 432  i3th7 549  i3orlem1 552  i3orlem2 553  i3orlem3 554  i3orlem8 559  ud3lem1c 568  ud3lem1d 569  ud3lem3d 575  ud3lem3 576  ud4lem1b 578  ud4lem1 581  ud5lem1b 587  ud5lem1 589  u4lemona 628  u1lemob 630  u5lemob 634  i2bi 722  u4lem2 747  u4lem5 764  u4lem6 768  u24lem 770  i2i1i1 800  test 802  test2 803  3vth1 804  mlalem 832  sa5 836  negantlem9 859  negantlem10 861  neg3antlem2 865  elimcons2 869  comanblem1 870  mhlem 876  mh 879  mlaconjo 886  cancellem 891  e2astlem1 895  gomaex3h7 908  gomaex3h11 912  gomaex3lem4 917  oat 927  oaidlem2 931  oaidlem2g 932  oa4lem2 938  oa4lem3 939  distoah3 942  oa3to4lem1 945  oa3to4lem2 946  oa4to6lem1 960  oa4to6lem2 961  oa4to6lem3 962  oa3-u1lem 985  d4oa 996  oadist2b 1008  oagen1 1014  oadist 1019  oadistb 1020  oadistd 1023  oa4cl 1027  4oagen1 1041  4oadist 1043  lem3.3.7i4e1 1068  lem4.6.6i0j2 1086  lem4.6.6i2j0 1092  lem4.6.6i2j1 1093  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  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  df-le2 131

Copyright terms: Public domain