Theorem lel2or 162

Description: Disjunction of 2 l.e.'s

Hypotheses

Ref	Expression
lel2.1	a ≤ b
lel2.2	c ≤ b

Assertion

Ref	Expression
lel2or	(a ∪ c) ≤ b

Proof of Theorem lel2or

Step	Hyp	Ref	Expression
1		lel2.1	. . 3 a ≤ b
2		lel2.2	. . 3 c ≤ b
3	1, 2	le2or 160	. 2 (a ∪ c) ≤ (b ∪ b)
4		oridm 102	. 2 (b ∪ b) = b
5	3, 4	lbtr 131	1 (a ∪ c) ≤ b

Syntax hints:   ≤ wle 2   ∪ wo 6

This theorem is referenced by:  womao 212  womaon 213  womaa 214  womaan 215  anorabs2 216  anorabs 217  mccune2 239  nom14 303  i2or 336  i1or 337  i5lei1 339  i5lei2 340  wdf-c2 366  cmtr1com 475  i0cmtrcom 477  ud3lem1c 550  ud3lem3 558  ud4lem1c 561  ud4lem1 563  ud5lem1 571  u3lemana 589  u4lemab 595  u5lemab 596  u3lemona 609  u4lemona 610  u5lemona 611  u4lemob 615  u5lemob 616  i2bi 704  u4lem1 719  u4lem5 746  u4lem6 750  u12lem 753  u3lem13a 771  u3lem13b 772  3vded11 796  3vded12 797  3vded22 800  1oa 802  mlalem 814  sa5 818  sadm3 820  negantlem2 831  negantlem4 833  negantlem9 841  negantlem10 843  neg3antlem2 847  neg3ant1 848  mhlem2 860  mh 861  cancellem 873  kb10iii 875  gomaex3lem2 895  oas 905  oatr 908  oaur 910  oal42 915  oa3to4lem4 928  oa4b 939  oa4to4u2 954  oa3-u1lem 965  oa3-u1 971  oa3-u2 972  oa3-1to5 973  d4oa 976  oadist2b 988  mloa 998

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-a 39  df-t 40  df-f 41  df-le1 122  df-le2 123

metamath.org