Theorem leror 144

Description: Add disjunct to right of both sides

Hypothesis

Ref	Expression
le.1	a ≤ b

Assertion

Ref	Expression
leror	(a ∪ c) ≤ (b ∪ c)

Proof of Theorem leror

Step	Hyp	Ref	Expression
1		orordir 105	. . . 4 ((a ∪ b) ∪ c) = ((a ∪ c) ∪ (b ∪ c))
2	1	ax-r1 34	. . 3 ((a ∪ c) ∪ (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 ∪ c) ∪ (b ∪ c)) = (b ∪ c)
7	6	df-le1 122	1 (a ∪ c) ≤ (b ∪ c)

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem is referenced by:  lelor 158  le2or 160  ka4lemo 220  ska13 233  wql2lem 280  womle2a 287  nom24 309  i5lei1 339  i5lei2 340  i5lei3 341  ska2 414  ska4 415  ka4ot 417  cmtr1com 475  ud4lem3a 565  ud4lem3b 566  comi1 691  3vded21 799  3vded22 800  3vroa 813  sa5 818  negantlem2 831  negantlem3 832  negantlem9 841  elimconslem 849  elimcons 850  comanb 854  oa4uto4g 955  oagen1 994  4oagen1 1021

This theorem was proved from axioms:  ax-a1 29  ax-a2 30  ax-a3 31  ax-a5 33  ax-r1 34  ax-r2 35  ax-r4 36  ax-r5 37

This theorem depends on definitions:  df-t 40  df-f 41  df-le1 122  df-le2 123

metamath.org