Theorem leror 152

Description: Add disjunct to right of both sides

Hypothesis

Ref	Expression
le.1	a =< b

Assertion

Ref	Expression
leror	(a v c) =< (b v c)

Proof of Theorem leror

Step	Hyp	Ref	Expression
1		orordir 113	. . . 4 ((a v b) v c) = ((a v c) v (b v c))
2	1	ax-r1 35	. . 3 ((a v c) v (b v c)) = ((a v b) v c)
3		le.1	. . . . 5 a =< b
4	3	df-le2 131	. . . 4 (a v b) = b
5	4	ax-r5 38	. . 3 ((a v b) v c) = (b v c)
6	2, 5	ax-r2 36	. 2 ((a v c) v (b v c)) = (b v c)
7	6	df-le1 130	1 (a v c) =< (b v c)

Syntax hints:   =< wle 2   v wo 6

This theorem is referenced by:  lelor 166  le2or 168  ka4lemo 228  ska13 241  wql2lem 288  womle2a 295  nom24 317  i5lei1 347  i5lei2 348  i5lei3 349  ska2 432  ska4 433  ka4ot 435  cmtr1com 493  ud4lem3a 583  ud4lem3b 584  comi1 709  3vded21 817  3vded22 818  3vroa 831  sa5 836  negantlem2 849  negantlem3 850  negantlem9 859  elimconslem 867  elimcons 868  comanb 872  e2ast2 894  oa4uto4g 975  oagen1 1014  4oagen1 1041  lem3.3.3lem1 1048  lem3.3.3lem2 1049

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-t 41  df-f 42  df-le1 130  df-le2 131

Copyright terms: Public domain