Theorem leao1 162

Description: L.e. absorption.

Assertion

Ref	Expression
leao1	(a ^ b) =< (a v c)

Proof of Theorem leao1

Step	Hyp	Ref	Expression
1		lea 160	. 2 (a ^ b) =< a
2		leo 158	. 2 a =< (a v c)
3	1, 2	letr 137	1 (a ^ b) =< (a v c)

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

This theorem is referenced by:  biao 799  mlaconj4 844  negantlem9 859  neg3antlem2 865  elimconslem 867  mhlem 876  mh 879  mlaconjolem 885  mlaconjo 886  lem4.6.2e1 1079  lem4.6.6i0j2 1086  lem4.6.6i0j3 1087  lem4.6.6i0j4 1088  lem4.6.6i2j0 1092  lem4.6.6i2j1 1093  lem4.6.6i2j4 1094  lem4.6.6i3j0 1095  lem4.6.6i3j1 1096  lem4.6.6i4j0 1097  lem4.6.6i4j2 1098

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