Theorem leao4 165

Description: L.e. absorption.

Assertion

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

Proof of Theorem leao4

Step	Hyp	Ref	Expression
1		lear 161	. 2 (b ^ a) =< a
2		leor 159	. 2 a =< (c v a)
3	1, 2	letr 137	1 (b ^ a) =< (c v a)

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

This theorem is referenced by:  k1-4 359  u3lem15 795  bi4 840  negantlem9 859  negantlem10 861  mh 879  marsdenlem4 883  cancellem 891  e2ast2 894  lem4.6.6i0j4 1088  lem4.6.6i2j4 1094  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