Theorem ler 141

Description: Add disjunct to right of l.e.

Hypothesis

Ref	Expression
le.1	a ≤ b

Assertion

Ref	Expression
ler	a ≤ (b ∪ c)

Proof of Theorem ler

Step	Hyp	Ref	Expression
1		ax-a3 31	. . . 4 ((a ∪ b) ∪ c) = (a ∪ (b ∪ c))
2	1	ax-r1 34	. . 3 (a ∪ (b ∪ c)) = ((a ∪ b) ∪ c)
3		le.1	. . . . 5 a ≤ b
4	3	df-le2 123	. . . 4 (a ∪ b) = b
5	4	ax-r5 37	. . 3 ((a ∪ b) ∪ c) = (b ∪ c)
6	2, 5	ax-r2 35	. 2 (a ∪ (b ∪ c)) = (b ∪ c)
7	6	df-le1 122	1 a ≤ (b ∪ c)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem is referenced by:  lerr 142  i3orlem4 537  i3orlem7 540  i3orlem8 541  negantlem9 841  negantlem10 843  neg3antlem2 847  mhlemlem1 856

This theorem was proved from axioms:  ax-a3 31  ax-r1 34  ax-r2 35  ax-r5 37

This theorem depends on definitions:  df-le1 122  df-le2 123

metamath.org