Theorem lel2or 170

Description: Disjunction of 2 l.e.'s. (Contributed by NM, 11-Nov-1997.)

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 168	. 2 (a ∪ c) ≤ (b ∪ b)
4		oridm 110	. 2 (b ∪ b) = b
5	3, 4	lbtr 139	1 (a ∪ c) ≤ b

Syntax hints:   ≤ wle 2   ∪ wo 6

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

This theorem is referenced by:  womao  220  womaon  221  womaa  222  womaan  223  anorabs2  224  mccune2  247  nom14  311  i2or  344  i1or  345  i5lei1  347  i5lei2  348  k1-2  357  k1-3  358  wdf-c2  384  cmtr1com  493  i0cmtrcom  495  ud3lem1c  568  ud3lem3  576  ud4lem1c  579  ud4lem1  581  ud5lem1  589  u3lemana  607  u4lemab  613  u5lemab  614  u3lemona  627  u4lemona  628  u5lemona  629  u4lemob  633  u5lemob  634  i2bi  722  u4lem1  737  u4lem5  764  u4lem6  768  u12lem  771  u3lem13a  789  u3lem13b  790  3vded11  814  3vded12  815  3vded22  818  1oa  820  mlalem  832  sa5  836  sadm3  838  negantlem2  849  negantlem4  851  negantlem9  859  negantlem10  861  neg3antlem2  865  neg3ant1  866  mhlem2  878  mh  879  cancellem  891  kb10iii  893  gomaex3lem2  915  oas  925  oatr  928  oaur  930  oal42  935  oa3to4lem4  948  oa4b  959  oa4to4u2  974  oa3-u1lem  985  oa3-u1  991  oa3-u2  992  oa3-1to5  993  d4oa  996  oadist2b  1008  mloa  1018  oa3moa3  1029  lem3.3.7i4e1  1069  lem4.6.6i0j1  1088  lem4.6.6i0j2  1089  lem4.6.6i0j3  1090  lem4.6.6i0j4  1091  lem4.6.6i1j3  1094  lem4.6.6i2j0  1095  lem4.6.6i2j1  1096  lem4.6.6i2j4  1097  lem4.6.6i3j0  1098  lem4.6.6i3j1  1099  lem4.6.6i4j0  1100  lem4.6.6i4j2  1101  lem4.6.7  1103  ml  1123  ml3le  1129  vneulem6  1136  vneulemexp  1148  dp53lema  1163  dp53lemf  1168  dp35lemf  1172  dp35lemd  1174  dp35lema  1178  dp41lemc  1185  xdp41  1198  xdp53  1200  xxdp41  1201  xxdp53  1203  xdp45lem  1204  xdp43lem  1205  xdp45  1206  xdp43  1207  3dp43  1208  oadp35lemf  1210